:: TOPMETR3  semantic presentation begin  
theorem :: TOPMETR3:1 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "X")) ")" )  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "S"))  ($#k2_tbsp_1 :::"."::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))  ")" ) & (Bool (Set (Var "F")) "is"   ($#v4_pre_topc :::"closed"::: )  )) "holds"  (Bool (Set   ($#k1_tbsp_1 :::"lim"::: )  (Set (Var "S")))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))))) ; 
 
theorem :: TOPMETR3:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "S"))) "is"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "Y")))))) ; 
 
theorem :: TOPMETR3:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "Y")) ")" )  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "T")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  ) & (Bool (Set (Var "T"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "S")))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  ))))) ; 
 
theorem :: TOPMETR3:4 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  "st" (Bool (Bool (Set (Var "s"))  ($#r1_funct_2 :::"="::: )  (Set (Var "S")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "implies" (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )) "implies" (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "implies" (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tbsp_1 :::"lim"::: )  (Set (Var "S"))))  ")"   ")" ))) ; 
 
theorem :: TOPMETR3:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  "st" (Bool (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "s")))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Var "s")) "is"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )))) ; 
 
theorem :: TOPMETR3:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set (Var "S")) "is"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k8_metric_1 :::"RealSpace"::: ) )))) ; 
 
theorem :: TOPMETR3:7 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "S1")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_funct_2 :::"="::: )  (Set (Var "S1"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )) "implies" (Bool (Set (Var "S1")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "S1")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )) "implies" (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )) "implies" (Bool (Set   ($#k1_tbsp_1 :::"lim"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tbsp_1 :::"lim"::: )  (Set (Var "S1"))))  ")"   ")" )))) ; 
 
theorem :: TOPMETR3:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_funct_2 :::"="::: )  (Set (Var "s"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  ) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_tbsp_1 :::"lim"::: )  (Set (Var "S"))))  ")" )))) ; 
 
theorem :: TOPMETR3:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_funct_2 :::"="::: )  (Set (Var "s"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "s")) "is"   ($#v7_valued_0 :::"non-decreasing"::: )  )) "holds"  (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )))) ; 
 
theorem :: TOPMETR3:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::)  (Bool  "for" (Set (Var "S")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  "st" (Bool (Bool (Set (Var "S"))  ($#r1_funct_2 :::"="::: )  (Set (Var "s"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "s")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  )) "holds"  (Bool (Set (Var "S")) "is"   ($#v2_tbsp_1 :::"convergent"::: )  )))) ; 
 
theorem :: TOPMETR3:11 (Bool  "for" (Set (Var "R")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v4_xxreal_2 :::"bounded_above"::: )  )) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v7_valued_0 :::"non-decreasing"::: )  ) & (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "s")))  ($#r1_tarski :::"c="::: )  (Set (Var "R"))) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_seq_4 :::"upper_bound"::: )  (Set (Var "R"))))  ")" ))) ; 
 
theorem :: TOPMETR3:12 (Bool  "for" (Set (Var "R")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v3_xxreal_2 :::"bounded_below"::: )  )) "holds"  (Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "s")) "is"   ($#v8_valued_0 :::"non-increasing"::: )  ) & (Bool (Set (Var "s")) "is"   ($#v2_comseq_2 :::"convergent"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "s")))  ($#r1_tarski :::"c="::: )  (Set (Var "R"))) & (Bool (Set   ($#k2_seq_2 :::"lim"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_seq_4 :::"lower_bound"::: )  (Set (Var "R"))))  ")" ))) ; 
 
theorem :: TOPMETR3:13 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_subset_1 :::"Real":::)  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r1"))) & (Bool (Set (Var "r2"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r2"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r1")))  ($#r2_hidden :::"in"::: )  (Set (Var "F1"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r2")))  ($#r2_hidden :::"in"::: )  (Set (Var "F2"))) & (Bool (Set (Var "F1")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "F2")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "F1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "F2")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "("  (Bool (Set (Var "r1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r2"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "F1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "F2"))))  ")" )))))) ; 
 
theorem :: TOPMETR3:14 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "P")) "," (Set (Var "P1")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "P1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set (Var "p2")) "," (Set (Var "p1"))) & (Bool (Set (Var "P1"))  ($#r1_tarski :::"c="::: )  (Set (Var "P")))) "holds"  (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set (Var "P")))))) ; 
 
theorem :: TOPMETR3:15 (Bool  "for" (Set (Var "P")) "," (Set (Var "P1")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set (Var "P")) "is"   ($#v1_topreal2 :::"being_simple_closed_curve"::: )  ) & (Bool (Set (Var "P1"))  ($#r1_topreal1 :::"is_an_arc_of"::: )  (Set   ($#k18_pscomp_1 :::"W-min"::: )  (Set (Var "P"))) "," (Set   ($#k22_pscomp_1 :::"E-max"::: )  (Set (Var "P")))) & (Bool (Set (Var "P1"))  ($#r1_tarski :::"c="::: )  (Set (Var "P"))) & (Bool (Bool  "not" (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_jordan6 :::"Upper_Arc"::: )  (Set (Var "P")))))) "holds"  (Bool (Set (Var "P1"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_jordan6 :::"Lower_Arc"::: )  (Set (Var "P"))))) ;