(continuity_ms_def
 (continuous_at?_TCC1 0
  (continuous_at?_TCC1-1 nil 3293829788
   ("" (skeep)
    (("" (lemma "fullset_metric_space1") (("" (propax) nil nil)) nil))
    nil)
   ((fullset_metric_space1 formula-decl nil continuity_ms_def nil))
   shostak))
 (continuous_at?_TCC2 0
  (continuous_at?_TCC2-1 nil 3459596827
   ("" (skeep)
    (("" (lemma "fullset_metric_space2") (("" (propax) nil nil)) nil))
    nil)
   ((fullset_metric_space2 formula-decl nil continuity_ms_def nil))
   nil))
 (continuous_at?_TCC3 0
  (continuous_at?_TCC3-1 nil 3459596827 ("" (subtype-tcc) nil nil)
   ((fullset const-decl "set" sets nil)) nil)))