:: METRIZTS  semantic presentation begin  





































definitionlet "T1", "T2" be   ($#l1_pre_topc :::"TopSpace":::); let "A1" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T1")); let "A2" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T2")); pred "A1" "," "A2" :::"are_homeomorphic":::  means :: METRIZTS:def 1 (Bool (Set "T1"  ($#k1_pre_topc :::"|"::: )  "A1") "," (Set "T2"  ($#k1_pre_topc :::"|"::: )  "A2")  ($#r1_borsuk_3 :::"are_homeomorphic"::: )  ); end; 







:: deftheorem    defines :::"are_homeomorphic"::: METRIZTS:def 1 :  (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "A2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2")) "holds"   (Bool  "("  (Bool (Set (Var "A1")) "," (Set (Var "A2"))  ($#r1_metrizts :::"are_homeomorphic"::: )  ) "iff" (Bool (Set (Set (Var "T1"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A1"))) "," (Set (Set (Var "T2"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A2")))  ($#r1_borsuk_3 :::"are_homeomorphic"::: )  )  ")" )))); 
 
theorem :: METRIZTS:1 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "T1")) "," (Set (Var "T2"))  ($#r1_borsuk_3 :::"are_homeomorphic"::: )  ) "iff" (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1"))) "," (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")))  ($#r1_metrizts :::"are_homeomorphic"::: )  )  ")" )) ; 
 
theorem :: METRIZTS:2 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "T1"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A1")) ")" ) "," (Set  "(" (Set (Var "T2"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A1")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "A1"))))) "holds"  (Bool (Set (Var "g")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))))) ; 
 
theorem :: METRIZTS:3 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool (Set (Var "A1")) "," (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A1")))  ($#r1_metrizts :::"are_homeomorphic"::: )  )))) ; 
 
theorem :: METRIZTS:4 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T1")) "," (Set (Var "T2"))  ($#r1_borsuk_3 :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "T2"))))) ; 
 registration
cluster   ($#v2_struct_0 :::"empty"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    ->   ($#v3_pcomps_1 :::"metrizable"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 

cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    ->   ($#v12_pre_topc :::"T_4"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
let "M" be   ($#l1_metric_1 :::"MetrSpace":::); 
cluster (Set   ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  "M") ->   ($#v3_pcomps_1 :::"metrizable"::: )   ; 
end; registrationlet "TM" be   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::); let "Am" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TM")); 
cluster (Set "TM"  ($#k1_pre_topc :::"|"::: )  "Am") ->   ($#v3_pcomps_1 :::"metrizable"::: )   ; 
end; registrationlet "TM1", "TM2" be   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "TM1" "," "TM2" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v3_pcomps_1 :::"metrizable"::: )   ; 
end; registrationlet "T" be   ($#v2_struct_0 :::"empty"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k2_waybel23 :::"weight"::: )  "T") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: METRIZTS:5 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_ordinal1 :::"c="::: )  (Set (Set  "("  ($#k2_waybel23 :::"weight"::: )  (Set (Var "T1")) ")" )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k2_waybel23 :::"weight"::: )  (Set (Var "T2")) ")" )))) ; 
 
theorem :: METRIZTS:6 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "T1")) "is"   ($#v2_struct_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set (Var "T2")) "is"   ($#v2_struct_0 :::"empty"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "T1")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k2_waybel23 :::"weight"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))) & (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "T2")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k2_waybel23 :::"weight"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) )))  ")" )) ; 
 registrationlet "T1", "T2" be   ($#v5_waybel23 :::"second-countable"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "T1" "," "T2" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v5_waybel23 :::"second-countable"::: )   ; 
end; 
theorem :: METRIZTS:7 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "F"))  ($#k1_tops_2 :::"|"::: )  (Set (Var "A")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "F"))))))) ; 
 
theorem :: METRIZTS:8 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "Bas")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set (Var "Bas"))  ($#k1_tops_2 :::"|"::: )  (Set (Var "A"))) "is"   ($#m1_subset_1 :::"Basis":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ))))) ; 
 registrationlet "T" be   ($#v5_waybel23 :::"second-countable"::: )    ($#l1_pre_topc :::"TopSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "A") ->   ($#v5_waybel23 :::"second-countable"::: )   ; 
end; 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  "("  ($#k3_pcomps_1 :::"TopSpaceMetr"::: )  (Set (Const "M")) ")" ); 
cluster (Set   ($#k6_weierstr :::"dist_min"::: )  "A") ->   ($#v5_pre_topc :::"continuous"::: )   ; 
end; 
theorem :: METRIZTS:9 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B"))))))) ; 
 registrationlet "TM" be   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v3_pre_topc :::"open"::: )    ->   ($#v5_topgen_4 :::"F_sigma"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "TM")); 

cluster   ($#v4_pre_topc :::"closed"::: )    ->   ($#v6_topgen_4 :::"G_delta"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "TM")); 
end; 
theorem :: METRIZTS:10 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v5_topgen_4 :::"F_sigma"::: )  ) & (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "F")) "is"   ($#v5_topgen_4 :::"F_sigma"::: )  )))) ; 
 
theorem :: METRIZTS:11 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "B")) ")" )  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v6_topgen_4 :::"G_delta"::: )  ) & (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "F")) "is"   ($#v6_topgen_4 :::"G_delta"::: )  )))) ; 
 
theorem :: METRIZTS:12 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v7_pre_topc :::"T_1"::: )  ) & (Bool (Set (Var "A")) "is"   ($#v2_tex_2 :::"discrete"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ) ")" )))) ; 
 
theorem :: METRIZTS:13 (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T")))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "G")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C")))  ")" ))  ")" )) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "A")) "is"   ($#v2_tex_2 :::"discrete"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C")))))) ; 
 
theorem :: METRIZTS:14 (Bool  "for" (Set (Var "iC")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "for" (Set (Var "Am")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Am")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "Am")) "is"   ($#v2_tex_2 :::"discrete"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Am")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC")))  ")" )) "holds"  (Bool  "for" (Set (Var "Am")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Am")) "is"   ($#v2_tex_2 :::"discrete"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Am")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC")))))) ; 
 
theorem :: METRIZTS:15 (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_tex_2 :::"discrete"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C")))  ")" )) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Bool  "not" (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "F"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))  ")" )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "F")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C")))))) ; 
 
theorem :: METRIZTS:16 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T")))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "G")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")) ")" )))  ")" )))) ; 
 
theorem :: METRIZTS:17 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Am")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Am")) "is"   ($#v1_tops_1 :::"dense"::: )  )) "holds"  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "TM")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set  ($#k4_ordinal1 :::"omega"::: ) )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Am")) ")" ))))) ; 
 begin  
theorem :: METRIZTS:18 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "iC")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "TM")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))) "iff" (Bool  "for" (Set (Var "Fm")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Fm")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "Fm")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM")))) "holds"  (Bool  "ex" (Set (Var "Gm")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "Gm"))  ($#r1_tarski :::"c="::: )  (Set (Var "Fm"))) & (Bool (Set (Var "Gm")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gm")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC")))  ")" )))  ")" ))) ; 
 
theorem :: METRIZTS:19 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "iC")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "TM")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))) "iff" (Bool  "for" (Set (Var "Am")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Am")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "Am")) "is"   ($#v2_tex_2 :::"discrete"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Am")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))))  ")" ))) ; 
 
theorem :: METRIZTS:20 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "iC")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "TM")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))) "iff" (Bool  "for" (Set (Var "Am")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Am")) "is"   ($#v2_tex_2 :::"discrete"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Am")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))))  ")" ))) ; 
 
theorem :: METRIZTS:21 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "iC")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "TM")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))) "iff" (Bool  "for" (Set (Var "Fm")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Fm")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Bool  "not" (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "Fm")))) & (Bool  "("   "for" (Set (Var "Am")) "," (Set (Var "Bm")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Am"))  ($#r2_hidden :::"in"::: )  (Set (Var "Fm"))) & (Bool (Set (Var "Bm"))  ($#r2_hidden :::"in"::: )  (Set (Var "Fm"))) & (Bool (Set (Var "Am"))  ($#r1_hidden :::"<>"::: )  (Set (Var "Bm")))) "holds"  (Bool (Set (Var "Am"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Bm")))  ")" )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Fm")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))))  ")" ))) ; 
 
theorem :: METRIZTS:22 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "iC")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_waybel23 :::"weight"::: )  (Set (Var "TM")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC"))) "iff" (Bool (Set   ($#k4_topgen_1 :::"density"::: )  (Set (Var "TM")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC")))  ")" ))) ; 
 
theorem :: METRIZTS:23 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "iC")) "being"   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "TM"))  "st" (Bool (Bool  "("   "for" (Set (Var "Fm")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Fm")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "Fm")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM")))) "holds"  (Bool  "ex" (Set (Var "Gm")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "Gm"))  ($#r1_tarski :::"c="::: )  (Set (Var "Fm"))) & (Bool (Set (Var "Gm")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gm")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC")))  ")" ))  ")" )) "holds"  (Bool  "ex" (Set (Var "underB")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "underB"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "underB")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "iC")))  ")" ))))) ; 
 begin  definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); attr "T" is  :::"Lindelof":::  means :: METRIZTS:def 2 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "T"  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" "T")) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "T" "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" "T") & (Bool (Set (Var "G")) "is"   ($#v4_card_3 :::"countable"::: )  )  ")" ))); end; 




:: deftheorem    defines :::"Lindelof"::: METRIZTS:def 2 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v1_metrizts :::"Lindelof"::: )  ) "iff" (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T")))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "G")) "is"   ($#v4_card_3 :::"countable"::: )  )  ")" )))  ")" )); 
 
theorem :: METRIZTS:24 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v1_metrizts :::"Lindelof"::: )  )) "holds"  (Bool  "ex" (Set (Var "B9")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "B9"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B9")) "is"   ($#v4_card_3 :::"countable"::: )  )  ")" )))) ; 
 registration
cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_pcomps_1 :::"metrizable"::: )     ($#v1_metrizts :::"Lindelof"::: )    ->   ($#v5_waybel23 :::"second-countable"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_pcomps_1 :::"metrizable"::: )     ($#v1_metrizts :::"Lindelof"::: )    ->   ($#v7_topgen_1 :::"separable"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 

cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v7_topgen_1 :::"separable"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    ->   ($#v3_pcomps_1 :::"metrizable"::: )     ($#v1_metrizts :::"Lindelof"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_pcomps_1 :::"metrizable"::: )     ($#v1_metrizts :::"Lindelof"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 

cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v5_waybel23 :::"second-countable"::: )    ->   ($#v1_metrizts :::"Lindelof"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 

cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v9_pre_topc :::"regular"::: )     ($#v1_metrizts :::"Lindelof"::: )    ->   ($#v10_pre_topc :::"normal"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 

cluster   ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v1_orders_4 :::"countable"::: )    ->   ($#v1_metrizts :::"Lindelof"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) "#)" ) ->   ($#v5_waybel23 :::"second-countable"::: )   ; 
end; registrationlet "T" be   ($#v1_metrizts :::"Lindelof"::: )    ($#l1_pre_topc :::"TopSpace":::); let "A" be   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "A") ->   ($#v1_metrizts :::"Lindelof"::: )   ; 
end; registrationlet "TM" be   ($#v3_pcomps_1 :::"metrizable"::: )     ($#v1_metrizts :::"Lindelof"::: )    ($#l1_pre_topc :::"TopSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TM")); 
cluster (Set "TM"  ($#k1_pre_topc :::"|"::: )  "A") ->   ($#v1_metrizts :::"Lindelof"::: )   ; 
end; definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "A", "B", "L" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); pred "L" :::"separates"::: "A" "," "B" means :: METRIZTS:def 3 (Bool  "ex" (Set (Var "U")) "," (Set (Var "W")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" "T" "st"  (Bool  "("  (Bool "A"  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool "B"  ($#r1_tarski :::"c="::: )  (Set (Var "W"))) & (Bool (Set (Var "U"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "W"))) & (Bool "L"  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "U"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "W")) ")" )  ($#k3_subset_1 :::"`"::: )  ))  ")" )); end; 







:: deftheorem    defines :::"separates"::: METRIZTS:def 3 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "L")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "L"))  ($#r2_metrizts :::"separates"::: )  (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool  "ex" (Set (Var "U")) "," (Set (Var "W")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "W"))) & (Bool (Set (Var "U"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "W"))) & (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "U"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "W")) ")" )  ($#k3_subset_1 :::"`"::: )  ))  ")" ))  ")" ))); 
 
theorem :: METRIZTS:25 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Am")) "," (Set (Var "Bm")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "Am")) "," (Set (Var "Bm"))  ($#r1_connsp_1 :::"are_separated"::: )  )) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM")) "st" (Bool (Set (Var "L"))  ($#r2_metrizts :::"separates"::: )  (Set (Var "Am")) "," (Set (Var "Bm")))))) ; 
 
theorem :: METRIZTS:26 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  (Bool  "for" (Set (Var "V1")) "," (Set (Var "V2")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A1"))  ($#r1_tarski :::"c="::: )  (Set (Var "V1"))) & (Bool (Set (Var "A2"))  ($#r1_tarski :::"c="::: )  (Set (Var "V2"))) & (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "V1")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "V2"))))) "holds"  (Bool  "for" (Set (Var "mV1")) "," (Set (Var "mV2")) "," (Set (Var "mL")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "M")) ")" )  "st" (Bool (Bool (Set (Var "mV1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "V1")) ")" ))) & (Bool (Set (Var "mV2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "V2")) ")" ))) & (Bool (Set (Var "mL"))  ($#r2_metrizts :::"separates"::: )  (Set (Var "mV1")) "," (Set (Var "mV2")))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "L"))  ($#r2_metrizts :::"separates"::: )  (Set (Var "A1")) "," (Set (Var "A2"))) & (Bool (Set (Set (Var "M"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "L")))  ($#r1_tarski :::"c="::: )  (Set (Var "mL")))  ")" ))))))) ;