:: TOPDIM_2  semantic presentation begin  









definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Fx" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); attr "Fx" is  :::"finite-order":::  means :: TOPDIM_2:def 1 (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "Gx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "X"  "st" (Bool (Bool (Set (Var "Gx"))  ($#r1_tarski :::"c="::: )  "Fx") & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gx"))))) "holds"  (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "Gx"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))); end; 





:: deftheorem    defines :::"finite-order"::: TOPDIM_2:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Fx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "Fx")) "is"   ($#v1_topdim_2 :::"finite-order"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "Gx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Gx"))  ($#r1_tarski :::"c="::: )  (Set (Var "Fx"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gx"))))) "holds"  (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "Gx"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )))  ")" ))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_topdim_2 :::"finite-order"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  "X" ")" )); 

cluster   ($#v1_finset_1 :::"finite"::: )    ->   ($#v1_topdim_2 :::"finite-order"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  "X" ")" )); 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Fx" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); func  :::"order"::: "Fx" ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   means :: TOPDIM_2:def 2 (Bool  "("  (Bool  "("   "for" (Set (Var "Gx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "X"  "st" (Bool (Bool (Set it  ($#k1_xxreal_3 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gx")))) & (Bool (Set (Var "Gx"))  ($#r1_tarski :::"c="::: )  "Fx")) "holds"  (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "Gx"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" ) & (Bool  "ex" (Set (Var "Gx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" "X" "st"  (Bool  "("  (Bool (Set (Var "Gx"))  ($#r1_tarski :::"c="::: )  "Fx") & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gx")))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_xxreal_3 :::"+"::: )  (Num 1))) & (Bool  "("   "not" (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "Gx"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "or" (Bool (Set (Var "Gx")) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" )  ")" ))  ")" ) if (Bool "Fx" "is"   ($#v1_topdim_2 :::"finite-order"::: )  )  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  )); end; 






:: deftheorem    defines :::"order"::: TOPDIM_2:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Fx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_xxreal_0 :::"ext-real"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "Fx")) "is"   ($#v1_topdim_2 :::"finite-order"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_topdim_2 :::"order"::: )  (Set (Var "Fx")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "Gx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Set (Var "b3"))  ($#k1_xxreal_3 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gx")))) & (Bool (Set (Var "Gx"))  ($#r1_tarski :::"c="::: )  (Set (Var "Fx")))) "holds"  (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "Gx"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" ) & (Bool  "ex" (Set (Var "Gx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "Gx"))  ($#r1_tarski :::"c="::: )  (Set (Var "Fx"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gx")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b3"))  ($#k1_xxreal_3 :::"+"::: )  (Num 1))) & (Bool  "("   "not" (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "Gx"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "or" (Bool (Set (Var "Gx")) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" )  ")" ))  ")" )  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "Fx")) "is"   ($#v1_topdim_2 :::"finite-order"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_topdim_2 :::"order"::: )  (Set (Var "Fx")))) "iff" (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xxreal_0 :::"+infty"::: )  ))  ")" )  ")"   ")" )))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#v1_topdim_2 :::"finite-order"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "X")); 
cluster (Set (Set  "("  ($#k1_topdim_2 :::"order"::: )  "F" ")" )  ($#k1_xxreal_3 :::"+"::: )  (Num 1)) ->   ($#v7_ordinal1 :::"natural"::: )   ; 

cluster (Set   ($#k1_topdim_2 :::"order"::: )  "F") ->   ($#v1_xxreal_0 :::"ext-real"::: )     ($#v1_int_1 :::"integer"::: )   ; 
end; 
theorem :: TOPDIM_2:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Fx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k1_topdim_2 :::"order"::: )  (Set (Var "Fx")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "Fx")) "is"   ($#v1_topdim_2 :::"finite-order"::: )  )))) ; 
 
theorem :: TOPDIM_2:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Fx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set   ($#k1_topdim_2 :::"order"::: )  (Set (Var "Fx")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "Gx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "Gx"))  ($#r1_tarski :::"c="::: )  (Set (Var "Fx"))) & (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Gx"))))) "holds"  (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "Gx"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ))))) ; 
 
theorem :: TOPDIM_2:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "Fx")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "Fx"))) & (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "G"))))) "holds"  (Bool (Set   ($#k6_setfam_1 :::"meet"::: )  (Set (Var "G"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" )) "holds"  (Bool (Set   ($#k1_topdim_2 :::"order"::: )  (Set (Var "Fx")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))))) ; 
 begin  



























theorem :: TOPDIM_2:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool  "ex" (Set (Var "F")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v2_tops_2 :::"closed"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM"))) & (Bool (Set (Var "F")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "TM")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ))) ; 
 
theorem :: TOPDIM_2:5 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I"))) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I"))) & (Bool (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B"))) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )  ")" )))) ; 
 
theorem :: TOPDIM_2:6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set (Var "TM")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "TM")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")))) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B"))) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k3_xxreal_3 :::"-"::: )  (Num 1))) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: TOPDIM_2:7 (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set (Var "TM")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "F")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM"))) & (Bool (Set (Var "F")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "I"))  ($#k1_xxreal_3 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "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_xboole_0 :::"meets"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))  ")" )  ")" )))) ; 
 
theorem :: TOPDIM_2:8 (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Integer":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool  "ex" (Set (Var "F")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM"))) & (Bool (Set (Var "F")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "F")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "I"))  ($#k1_xxreal_3 :::"+"::: )  (Num 1)))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "TM")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I")))  ")" ))) ; 
 registrationlet "TM" be   ($#v5_waybel23 :::"second-countable"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::); let "A", "B" be   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "TM")); 
cluster (Set "A"  ($#k2_xboole_0 :::"\/"::: )  "B") ->   ($#v1_topdim_1 :::"finite-ind"::: )    for  ($#m1_subset_1 :::"Subset":::) "of" "TM"; 
end; 
theorem :: TOPDIM_2:9 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" )) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B"))) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "("  ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "("  ($#k2_topdim_1 :::"ind"::: )  (Set (Var "B")) ")" ) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Num 1)))  ")" ))) ; 
 
theorem :: TOPDIM_2:10 (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 (Set   ($#k2_tops_1 :::"Fr"::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "A1")) "," (Set (Var "A2")) ($#k3_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A1")) ")" ) "," (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A2")) ")" ) ($#k3_borsuk_1 :::":]"::: ) )  ($#k4_subset_1 :::"\/"::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A1")) ")" ) "," (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A2")) ")" ) ($#k3_borsuk_1 :::":]"::: ) )))))) ; 
 registrationlet "TM1", "TM2" be   ($#v5_waybel23 :::"second-countable"::: )     ($#v3_topdim_1 :::"finite-ind"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "TM1" "," "TM2" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v3_topdim_1 :::"finite-ind"::: )   ; 
end; 
theorem :: TOPDIM_2:11 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "H")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "H"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "H"))) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  )) "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 "A")) "," (Set (Var "B"))) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "L"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "H")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k3_xxreal_3 :::"-"::: )  (Num 1)))  ")" )))))) ; 
 
theorem :: TOPDIM_2:12 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Var "TM")) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v4_pre_topc :::"closed"::: )  ) & (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "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 "A")) "," (Set (Var "B"))) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "L")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k3_xxreal_3 :::"-"::: )  (Num 1)))  ")" ))))) ; 
 
theorem :: TOPDIM_2:13 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "H"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "H")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "TM"))  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "ex" (Set (Var "W")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set (Set (Var "H"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")) ")" )) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "H"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k3_xxreal_3 :::"-"::: )  (Num 1)))  ")" ))))  ")" )))) ; 
 
theorem :: TOPDIM_2:14 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "H"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "H")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ) "iff" (Bool  "ex" (Set (Var "Bas")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "TM")) "st"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "Bas")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "H"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A")) ")" )) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "H"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k3_xxreal_3 :::"-"::: )  (Num 1)))  ")" )))  ")" )))) ; 
 
theorem :: TOPDIM_2:15 (Bool  "for" (Set (Var "TM1")) "," (Set (Var "TM2")) "being"   ($#v5_waybel23 :::"second-countable"::: )     ($#v3_topdim_1 :::"finite-ind"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "("   "not" (Bool (Set (Var "TM1")) "is"   ($#v2_struct_0 :::"empty"::: )  ) "or"  "not" (Bool (Set (Var "TM2")) "is"   ($#v2_struct_0 :::"empty"::: )  )  ")" )) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "TM1")) "," (Set (Var "TM2")) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM1")) ")" )  ($#k1_xxreal_3 :::"+"::: )  (Set  "("  ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM2")) ")" )))) ; 
 
theorem :: TOPDIM_2:16 (Bool  "for" (Set (Var "TM2")) "," (Set (Var "TM1")) "being"   ($#v5_waybel23 :::"second-countable"::: )     ($#v3_topdim_1 :::"finite-ind"::: )     ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "TM1")) "," (Set (Var "TM2")) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM1"))))) ; 
 begin  













theorem :: TOPDIM_2:17 (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k14_euclid :::"Euclid"::: )  (Num 1) ")" )  (Bool  "for" (Set (Var "u1")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "u1")) ($#k9_finseq_1 :::"*>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "u")))) "holds"  (Bool (Set   ($#k10_metric_1 :::"cl_Ball"::: )   "(" (Set (Var "u")) "," (Set (Var "r")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) where s "is"   ($#m1_subset_1 :::"Real":::) : (Bool  "("  (Bool (Set (Set (Var "u1"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "r")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "s"))) & (Bool (Set (Var "s"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "u1"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "r"))))  ")" )  "}"  ))) ; 
 
theorem :: TOPDIM_2:18 (Bool  "for" (Set (Var "U")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Num 1) ")" )  (Bool  "for" (Set (Var "u1")) "," (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "u1")) ($#k9_finseq_1 :::"*>"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "U"))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set  "("  ($#k1_topreal9 :::"Ball"::: )   "(" (Set (Var "U")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k9_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "u1"))  ($#k3_xxreal_3 :::"-"::: )  (Set (Var "r")) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set  ($#k9_finseq_1 :::"<*"::: ) (Set  "(" (Set (Var "u1"))  ($#k1_xxreal_3 :::"+"::: )  (Set (Var "r")) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ($#k2_tarski :::"}"::: ) )))) ; 
 
theorem :: TOPDIM_2:19 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v4_card_3 :::"countable"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A"))) "is"   ($#v12_pre_topc :::"T_4"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 registrationlet "TM" be   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v4_card_3 :::"countable"::: )    ->   ($#v1_topdim_1 :::"finite-ind"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "TM")); 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") ->   ($#v3_topdim_1 :::"finite-ind"::: )   ; 
end; 
theorem :: TOPDIM_2:20 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Num 1))) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: TOPDIM_2:21 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) ; 
 
theorem :: TOPDIM_2:22 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A"))) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"    ($#m1_setfam_1 :::"Cover"::: )   "of" (Set (Var "A")))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "F")) "," (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "TM"))) ")" ) "st"  (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "g"))) "is"    ($#m1_setfam_1 :::"Cover"::: )   "of" (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "F")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Var "a")))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "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 (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b"))))  ")" )  ")" ))))) ; 
 
theorem :: TOPDIM_2:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set (Var "TM")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "TM")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM")))) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "TM"))) & (Bool (Set (Var "G"))  ($#r1_setfam_1 :::"is_finer_than"::: )  (Set (Var "F"))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "F")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set   ($#k1_topdim_2 :::"order"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ))))) ; 
 
theorem :: TOPDIM_2:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "TM")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set  "(" (Set (Var "A"))  ($#k3_subset_1 :::"`"::: )  ")" )) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) "holds"  (Bool  "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "A2"))))) "holds"  (Bool  "ex" (Set (Var "X1")) "," (Set (Var "X2")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM")) "st"  (Bool  "("  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "TM")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X1"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "X2")))) & (Bool (Set (Var "A1"))  ($#r1_tarski :::"c="::: )  (Set (Var "X1"))) & (Bool (Set (Var "A2"))  ($#r1_tarski :::"c="::: )  (Set (Var "X2"))) & (Bool (Set (Set (Var "A1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "X2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A2")))) & (Bool (Set (Set (Var "A1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A2")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A2")))) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set  "(" (Set (Var "X1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "X2")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "(" (Set (Var "A1"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A2")) ")" ) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k3_xxreal_3 :::"-"::: )  (Num 1)))  ")" )))))) ;