:: TOPMETR  semantic presentation begin  










theorem :: TOPMETR:1 (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "F"))))  ")" ))) ; 
 



theorem :: TOPMETR:2 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v8_pre_topc :::"T_2"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v8_pre_topc :::"T_2"::: )  ))) ; 
 
theorem :: TOPMETR:3 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "B"))))) "holds"  (Bool (Set (Var "A")) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "B"))))) ; 
 







theorem :: TOPMETR:4 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "P"))) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "P"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Q")) ")" ))) & (Bool (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Q"))) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "P"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Q")) ")" )))  ")" ))) ; 
 
theorem :: TOPMETR:5 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool  "for" (Set (Var "Q")) "being"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "p"))  (Bool  "for" (Set (Var "p9")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )  (Bool  "for" (Set (Var "Q9")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")) ")" )  "st" (Bool (Bool (Set (Var "Q9"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Q"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "P")))) & (Bool (Set (Var "p9"))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "Q9")) "is"    ($#m1_connsp_2 :::"a_neighborhood"::: )   "of" (Set (Var "p9"))))))))) ; 
 
theorem :: TOPMETR:6 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set  "(" (Set (Var "B"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "C")) ")" )  "st" (Bool (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) "holds"  (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  ))))) ; 
 
theorem :: TOPMETR:7 (Bool  "for" (Set (Var "X")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "K0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "K0")) ")" ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "K0"))))) "holds"  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))))) ; 
 





definitionlet "M" be   ($#l1_metric_1 :::"MetrSpace":::); mode  :::"SubSpace":::  "of" "M" ->   ($#l1_metric_1 :::"MetrSpace":::) means :: TOPMETR:def 1 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "M")) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" it "holds"  (Bool (Set (Set  "the"  ($#u1_metric_1 :::"distance"::: )  "of" it)  ($#k1_metric_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_metric_1 :::"distance"::: )  "of" "M")  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" )  ")" ); end; 





:: deftheorem    defines :::"SubSpace"::: TOPMETR:def 1 :  (Bool  "for" (Set (Var "M")) "," (Set (Var "b2")) "being"   ($#l1_metric_1 :::"MetrSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_topmetr :::"SubSpace"::: )   "of" (Set (Var "M"))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "M")))) & (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "b2")) "holds"  (Bool (Set (Set  "the"  ($#u1_metric_1 :::"distance"::: )  "of" (Set (Var "b2")))  ($#k1_metric_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_metric_1 :::"distance"::: )  "of" (Set (Var "M")))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" ))  ")" )  ")" )  ")" )); 
 registrationlet "M" be   ($#l1_metric_1 :::"MetrSpace":::); 
cluster   ($#v1_metric_1 :::"strict"::: )     ($#v6_metric_1 :::"Reflexive"::: )     ($#v7_metric_1 :::"discerning"::: )   bbbadV8_METRIC_1()   ($#v9_metric_1 :::"triangle"::: )    for    ($#m1_topmetr :::"SubSpace"::: )   "of" "M"; 
end; registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_metric_1 :::"strict"::: )     ($#v6_metric_1 :::"Reflexive"::: )     ($#v7_metric_1 :::"discerning"::: )   bbbadV8_METRIC_1()   ($#v9_metric_1 :::"triangle"::: )    for    ($#m1_topmetr :::"SubSpace"::: )   "of" "M"; 
end; 



theorem :: TOPMETR:8 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_topmetr :::"SubSpace"::: )   "of" (Set (Var "M"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Var "p")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")))))) ; 
 
theorem :: TOPMETR:9 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m1_topmetr :::"SubSpace"::: )   "of" (Set (Var "M"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "x9")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "x9")))) "holds"  (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "x9")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "x")) "," (Set (Var "r")) ")"  ")" )  ($#k8_subset_1 :::"/\"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "A")))))))))) ; 
 definitionlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); func "M" :::"|"::: "A" ->   ($#v1_metric_1 :::"strict"::: )     ($#m1_topmetr :::"SubSpace"::: )   "of" "M" means :: TOPMETR:def 2 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  "A"); end; 






:: deftheorem    defines :::"|"::: TOPMETR:def 2 :  (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_metric_1 :::"strict"::: )     ($#m1_topmetr :::"SubSpace"::: )   "of" (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k1_topmetr :::"|"::: )  (Set (Var "A")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  ")" )))); 
 registrationlet "M" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "M")); 
cluster (Set "M"  ($#k1_topmetr :::"|"::: )  "A") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_metric_1 :::"strict"::: )   ; 
end; definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; assume 
(Bool (Set (Const "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "b")))
 ; func  :::"Closed-Interval-MSpace":::  "(" "a" "," "b" ")"  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_metric_1 :::"strict"::: )     ($#m1_topmetr :::"SubSpace"::: )   "of" (Set   ($#k8_metric_1 :::"RealSpace"::: )  ) means :: TOPMETR:def 3 (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) "a" "," "b" ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  ($#k1_topmetr :::"|"::: )  (Set (Var "P"))))); end; 







:: deftheorem    defines :::"Closed-Interval-MSpace"::: TOPMETR:def 3 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_metric_1 :::"strict"::: )     ($#m1_topmetr :::"SubSpace"::: )   "of" (Set   ($#k8_metric_1 :::"RealSpace"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "for" (Set (Var "P")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  ($#k1_topmetr :::"|"::: )  (Set (Var "P")))))  ")" ))); 
 
theorem :: TOPMETR:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) ; 
 



definitionlet "M" be    ($#l1_metric_1 :::"MetrStruct"::: )  ; let "F" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "M")); attr "F" is  :::"being_ball-family":::  means :: TOPMETR:def 4 (Bool  "for" (Set (Var "P")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "P"))  ($#r2_hidden :::"in"::: )  "F")) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" "M"(Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" ))))); end; 





:: deftheorem    defines :::"being_ball-family"::: TOPMETR:def 4 :  (Bool  "for" (Set (Var "M")) "being"    ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_topmetr :::"being_ball-family"::: )  ) "iff" (Bool  "for" (Set (Var "P")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "P"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))(Bool  "ex" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" )))))  ")" ))); 
 
theorem :: TOPMETR:11 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k8_metric_1 :::"RealSpace"::: ) )  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) "holds"  (Bool (Set   ($#k4_metric_1 :::"dist"::: )   "(" (Set (Var "p")) "," (Set (Var "q")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "y")) ")" ))))) ; 
 
theorem :: TOPMETR:12 (Bool  "for" (Set (Var "M")) "being"    ($#l1_metric_1 :::"MetrStruct"::: )   "holds"   (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" ))) & (Bool (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_pcomps_1 :::"Family_open_set"::: )  (Set (Var "M"))))  ")" )) ; 
 
theorem :: TOPMETR:13 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#m1_topmetr :::"SubSpace"::: )   "of" (Set (Var "M")) "holds"  (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "A"))) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")))))) ; 
 
theorem :: TOPMETR:14 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#v9_metric_1 :::"triangle"::: )     ($#l1_metric_1 :::"MetrStruct"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" ))) "holds"  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ))))) ; 
 
theorem :: TOPMETR:15 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::)  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "P")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "P")))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k9_metric_1 :::"Ball"::: )   "(" (Set (Var "p")) "," (Set (Var "r")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "P")))  ")" )))  ")" ))) ; 
 definitionlet "M" be    ($#l1_metric_1 :::"MetrStruct"::: )  ; attr "M" is  :::"compact":::  means :: TOPMETR:def 5 (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  "M") "is"   ($#v1_compts_1 :::"compact"::: )  ); end; 




:: deftheorem    defines :::"compact"::: TOPMETR:def 5 :  (Bool  "for" (Set (Var "M")) "being"    ($#l1_metric_1 :::"MetrStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v2_topmetr :::"compact"::: )  ) "iff" (Bool (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Var "M"))) "is"   ($#v1_compts_1 :::"compact"::: )  )  ")" )); 
 
theorem :: TOPMETR:16 (Bool  "for" (Set (Var "M")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_metric_1 :::"MetrSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v2_topmetr :::"compact"::: )  ) "iff" (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_topmetr :::"being_ball-family"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "M")))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "M")) "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "M"))) & (Bool (Set (Var "G")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )))  ")" )) ; 
 definitionfunc  :::"R^1":::  ->   ($#l1_pre_topc :::"TopSpace":::) equals :: TOPMETR:def 6 (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set  ($#k8_metric_1 :::"RealSpace"::: ) )); end; 




:: deftheorem    defines :::"R^1"::: TOPMETR:def 6 :  (Bool (Set   ($#k3_topmetr :::"R^1"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set  ($#k8_metric_1 :::"RealSpace"::: ) ))); 
 registration
cluster (Set   ($#k3_topmetr :::"R^1"::: )  ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: TOPMETR:17 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k3_topmetr :::"R^1"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_numbers :::"REAL"::: )  )) ; 
 definitionlet "a", "b" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Closed-Interval-TSpace":::  "(" "a" "," "b" ")"  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )     ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k3_topmetr :::"R^1"::: )  ) equals :: TOPMETR:def 7 (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" "a" "," "b" ")"  ")" )); end; 






:: deftheorem    defines :::"Closed-Interval-TSpace"::: TOPMETR:def 7 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set  "("  ($#k2_topmetr :::"Closed-Interval-MSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )))); 
 
theorem :: TOPMETR:18 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) ; 
 
theorem :: TOPMETR:19 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b")))) "holds"  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool (Set (Var "P"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_topmetr :::"R^1"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "P")))))) ; 
 
theorem :: TOPMETR:20 (Bool (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k17_borsuk_1 :::"I[01]"::: )  )) ; 
 definition:: original: :::"I[01]"::: redefine func  :::"I[01]":::  ->    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k3_topmetr :::"R^1"::: )  ); end; 
theorem :: TOPMETR:21 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k3_topmetr :::"R^1"::: ) ) "," (Set  ($#k3_topmetr :::"R^1"::: ) )  "st" (Bool (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Real":::) "st"  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Real":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set (Var "x")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "b"))))))) "holds"  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) ; 
 
theorem :: TOPMETR:22 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A"))) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")))))) ; 
 
theorem :: TOPMETR:23 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "d")) "," (Set (Var "e")) ")"  ")" )  "st" (Bool (Bool (Set (Var "d"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "e"))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "d")) "," (Set (Var "e")) ")"  ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")))))) ; 
 
theorem :: TOPMETR:24 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )  "st" (Bool (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds"  (Bool (Set   ($#k4_topmetr :::"Closed-Interval-TSpace"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k5_topmetr :::"I[01]"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")))))) ; 
 definitionlet "T" be    ($#l1_struct_0 :::"1-sorted"::: )  ; attr "T" is  :::"real-membered":::  means :: TOPMETR:def 8 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") "is"   ($#v3_membered :::"real-membered"::: )  ); end; 




:: deftheorem    defines :::"real-membered"::: TOPMETR:def 8 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_struct_0 :::"1-sorted"::: )   "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_topmetr :::"real-membered"::: )  ) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "is"   ($#v3_membered :::"real-membered"::: )  )  ")" )); 
 registration
cluster (Set   ($#k17_borsuk_1 :::"I[01]"::: )  ) ->   ($#v3_topmetr :::"real-membered"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_topmetr :::"real-membered"::: )    for    ($#l1_struct_0 :::"1-sorted"::: )  ; 
end; registrationlet "S" be   ($#v3_topmetr :::"real-membered"::: )     ($#l1_struct_0 :::"1-sorted"::: )  ; 
cluster (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ->   ($#v3_membered :::"real-membered"::: )   ; 
end; registration
cluster (Set   ($#k3_topmetr :::"R^1"::: )  ) ->   ($#v3_topmetr :::"real-membered"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_topmetr :::"real-membered"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registrationlet "T" be   ($#v3_topmetr :::"real-membered"::: )     ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster   ->   ($#v3_topmetr :::"real-membered"::: )    for    ($#m1_pre_topc :::"SubSpace"::: )   "of" "T"; 
end; registration
cluster (Set   ($#k8_metric_1 :::"RealSpace"::: )  ) ->   ($#v3_topmetr :::"real-membered"::: )   ; 
end;