:: TOPDIM_1  semantic presentation begin  






























theorem :: TOPDIM_1:1 (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 "A")) ")" )  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "F")))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "B")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set (Var "A"))))))) ; 
 
theorem :: TOPDIM_1:2 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v10_pre_topc :::"normal"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (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   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "U")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_pre_topc :::"Cl"::: )  (Set (Var "W"))))  ")" )))  ")" )) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"Seq_of_ind"::: "T" ->   ($#m1_subset_1 :::"SetSequence":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ")" ) means :: TOPDIM_1:def 1 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set it  ($#k13_prob_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k1_struct_0 :::"{}"::: )  "T" ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool  "("   "not" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set it  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))) "or" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set it  ($#k13_prob_1 :::"."::: )  (Set (Var "n")))) "or" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" "T"  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" "T"  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "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  "(" "T"  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")))  ($#r2_hidden :::"in"::: )  (Set it  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))  ")" ))))  ")" ) &  "("  (Bool (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set it  ($#k13_prob_1 :::"."::: )  (Set (Var "n")))) "or" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" "T"  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" "T"  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "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  "(" "T"  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")))  ($#r2_hidden :::"in"::: )  (Set it  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))  ")" ))))  ")" )) "implies" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set it  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"   ")" ))); end; 





:: deftheorem    defines :::"Seq_of_ind"::: TOPDIM_1:def 1 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set  "("  ($#k9_setfam_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "b2"))  ($#k13_prob_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k1_struct_0 :::"{}"::: )  (Set (Var "T")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool  "("   "not" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b2"))  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))) "or" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b2"))  ($#k13_prob_1 :::"."::: )  (Set (Var "n")))) "or" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "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  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b2"))  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))  ")" ))))  ")" ) &  "("  (Bool (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b2"))  ($#k13_prob_1 :::"."::: )  (Set (Var "n")))) "or" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "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  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b2"))  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))  ")" ))))  ")" )) "implies" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "b2"))  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))  ")"   ")" )))  ")" ))); 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k1_topdim_1 :::"Seq_of_ind"::: )  "T") ->   ($#v3_prob_1 :::"non-descending"::: )   ; 
end; 
theorem :: TOPDIM_1:3 (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 "n")) "being"   ($#m1_hidden :::"Nat":::)  (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  "("  (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "n")))) "iff" (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))  ")" ))))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); attr "A" is  :::"with_finite_small_inductive_dimension":::  means :: TOPDIM_1:def 2 (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool "A"  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  "T" ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))); end; 





:: deftheorem    defines :::"with_finite_small_inductive_dimension"::: TOPDIM_1:def 2 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_topdim_1 :::"with_finite_small_inductive_dimension"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "n")))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); synonym  :::"finite-ind"::: "A" for  :::"with_finite_small_inductive_dimension"::: ; end; definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "G" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); attr "G" is  :::"with_finite_small_inductive_dimension":::  means :: TOPDIM_1:def 3 (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool "G"  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  "T" ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))); end; 





:: deftheorem    defines :::"with_finite_small_inductive_dimension"::: TOPDIM_1:def 3 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"with_finite_small_inductive_dimension"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "n")))))  ")" ))); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "G" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); synonym  :::"finite-ind"::: "G" for  :::"with_finite_small_inductive_dimension"::: ; end; 
theorem :: TOPDIM_1:4 (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 "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "G"))) & (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )))) ; 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v1_finset_1 :::"finite"::: )    ->   ($#v1_topdim_1 :::"finite-ind"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")); 

cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v2_topdim_1 :::"finite-ind"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ")" )); 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_topdim_1 :::"finite-ind"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ")" )); 
end; registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_topdim_1 :::"finite-ind"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")); 
end; definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); attr "T" is  :::"with_finite_small_inductive_dimension":::  means :: TOPDIM_1:def 4 (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  "T") "is"   ($#v1_topdim_1 :::"with_finite_small_inductive_dimension"::: )  ); end; 




:: deftheorem    defines :::"with_finite_small_inductive_dimension"::: TOPDIM_1:def 4 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"with_finite_small_inductive_dimension"::: )  ) "iff" (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T"))) "is"   ($#v1_topdim_1 :::"with_finite_small_inductive_dimension"::: )  )  ")" )); 
 notationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); synonym  :::"finite-ind"::: "T" for  :::"with_finite_small_inductive_dimension"::: ; end; registration
cluster   ($#v2_struct_0 :::"empty"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    ->   ($#v3_topdim_1 :::"finite-ind"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_compts_1 :::"1TopSp"::: )  "X") ->   ($#v3_topdim_1 :::"finite-ind"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v3_topdim_1 :::"finite-ind"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; 





begin  definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); assume 
(Bool (Set (Const "A")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )
 ; func  :::"ind"::: "A" ->   ($#m1_hidden :::"Integer":::) means :: TOPDIM_1:def 5 (Bool  "("  (Bool "A"  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  "T" ")" )  ($#k13_prob_1 :::"."::: )  (Set  "(" it  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Bool  "not" "A"  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  "T" ")" )  ($#k13_prob_1 :::"."::: )  it)))  ")" ); end; 







:: deftheorem    defines :::"ind"::: TOPDIM_1:def 5 :  (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 "A")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")))) "iff" (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "b3"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Bool  "not" (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "b3")))))  ")" )  ")" )))); 
 
theorem :: TOPDIM_1:5 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Af")))))) ; 
 
theorem :: TOPDIM_1:6 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Af")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) "iff" (Bool (Set (Var "Af")) "is"   ($#v1_xboole_0 :::"empty"::: )  )  ")" ))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set   ($#k2_topdim_1 :::"ind"::: )  "A") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 
theorem :: TOPDIM_1:7 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Af")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1))) "iff" (Bool (Set (Var "Af"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set (Var "n"))))  ")" )))) ; 
 
theorem :: TOPDIM_1:8 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "holds" (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))))) ; 
 
theorem :: TOPDIM_1:9 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Af")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Af")) ")" )  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Af")) ")" )  "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  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Af")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W"))) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1)))  ")" ))))  ")" )))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "G" be   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); assume 
(Bool (Set (Const "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  )
 ; func  :::"ind"::: "G" ->   ($#m1_hidden :::"Integer":::) means :: TOPDIM_1:def 6 (Bool  "("  (Bool "G"  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  "T" ")" )  ($#k13_prob_1 :::"."::: )  (Set  "(" it  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  it) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool "G"  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  "T" ")" )  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))  ")" )  ")" ); end; 







:: deftheorem    defines :::"ind"::: TOPDIM_1:def 6 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "b3"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" ))) & (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "b3"))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k1_topdim_1 :::"Seq_of_ind"::: )  (Set (Var "T")) ")" )  ($#k13_prob_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k3_real_1 :::"+"::: )  (Num 1) ")" )))) "holds"  (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i")))  ")" )  ")" )  ")" )))); 
 
theorem :: TOPDIM_1:10 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool  "("  (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Num 1))) & (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  )  ")" ) "iff" (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k1_struct_0 :::"{}"::: )  (Set (Var "T")) ")" ) ($#k6_domain_1 :::"}"::: ) ))  ")" ))) ; 
 
theorem :: TOPDIM_1:11 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I"))) "iff" (Bool  "("  (Bool (Set   ($#k1_real_1 :::"-"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I"))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "G")))) "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 (Var "I")))  ")" )  ")" )  ")" )  ")" )))) ; 
 
theorem :: TOPDIM_1:12 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G1")) "," (Set (Var "G2")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "G1")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Var "G2"))  ($#r1_tarski :::"c="::: )  (Set (Var "G1")))) "holds"  (Bool  "("  (Bool (Set (Var "G2")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G2")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G1"))))  ")" ))) ; 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "G1", "G2" be   ($#v2_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); 
cluster (Set "G1"  ($#k2_xboole_0 :::"\/"::: )  "G2") ->   ($#v2_topdim_1 :::"finite-ind"::: )    for  ($#m1_subset_1 :::"Subset-Family":::) "of" "T"; 
end; 
theorem :: TOPDIM_1:13 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "," (Set (Var "G1")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "I")) "being"   ($#m1_hidden :::"Integer":::)  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Var "G1")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I"))) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G1")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I")))) "holds"  (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "G"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "G1")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "I")))))) ; 
 definitionlet "T" be   ($#l1_pre_topc :::"TopSpace":::); func  :::"ind"::: "T" ->   ($#m1_hidden :::"Integer":::) equals :: TOPDIM_1:def 7 (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  "T" ")" )); end; 





:: deftheorem    defines :::"ind"::: TOPDIM_1:def 7 :  (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")) ")" )))); 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_topdim_1 :::"finite-ind"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k4_topdim_1 :::"ind"::: )  "T") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 
theorem :: TOPDIM_1:14 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  "("  ($#k1_compts_1 :::"1TopSp"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: TOPDIM_1:15 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "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 "T")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W"))) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1)))  ")" )))))) "holds"  (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  )) ; 
 
theorem :: TOPDIM_1:16 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Tf")) "being"   ($#v3_topdim_1 :::"finite-ind"::: )    ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "Tf")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Tf"))  (Bool  "for" (Set (Var "U")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Tf"))  "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 "Tf")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W"))) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1)))  ")" ))))  ")" ))) ; 
 begin  registrationlet "Tf" be   ($#v3_topdim_1 :::"finite-ind"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster   ->   ($#v1_topdim_1 :::"finite-ind"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "Tf")); 
end; registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "Af" be   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "Af") ->   ($#v3_topdim_1 :::"finite-ind"::: )   ; 
end; 
theorem :: TOPDIM_1:17 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Af")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Af")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Af")))))) ; 
 
theorem :: TOPDIM_1:18 (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 (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A"))) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ))) ; 
 
theorem :: TOPDIM_1:19 (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 "Af")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Af")))) "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   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Af"))))  ")" )))) ; 
 
theorem :: TOPDIM_1:20 (Bool  "for" (Set (Var "Tf")) "being"   ($#v3_topdim_1 :::"finite-ind"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Tf")) "holds"  (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "Tf")))))) ; 
 
theorem :: TOPDIM_1:21 (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"))) & (Bool (Set (Var "B")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "B"))))  ")" )))) ; 
 
theorem :: TOPDIM_1:22 (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"))) & (Bool (Set (Var "F")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "B"))))  ")" )))) ; 
 
theorem :: TOPDIM_1:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v9_pre_topc :::"regular"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Bool  "not" (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))) "holds"  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "L"))  ($#r2_metrizts :::"separates"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "p")) ($#k6_domain_1 :::"}"::: ) ) "," (Set (Var "A"))) & (Bool (Set (Var "L")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "L")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1)))  ")" ))))  ")" ))) ; 
 
theorem :: TOPDIM_1:24 (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  "("  (Bool (Set (Var "T1")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) "iff" (Bool (Set (Var "T2")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  )  ")" )) ; 
 
theorem :: TOPDIM_1:25 (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"::: )  ) & (Bool (Set (Var "T1")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T1")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T2"))))) ; 
 
theorem :: TOPDIM_1:26 (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"))  "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2"))  ($#r1_metrizts :::"are_homeomorphic"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "A1")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) "iff" (Bool (Set (Var "A2")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )  ")" )))) ; 
 
theorem :: TOPDIM_1:27 (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"))  "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2"))  ($#r1_metrizts :::"are_homeomorphic"::: )  ) & (Bool (Set (Var "A1")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A1")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A2"))))))) ; 
 
theorem :: TOPDIM_1:28 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  )) "holds"  (Bool  "("  (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T2")) "," (Set (Var "T1")) ($#k2_borsuk_1 :::":]"::: ) ) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_topdim_1 :::"ind"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T2")) "," (Set (Var "T1")) ($#k2_borsuk_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: TOPDIM_1:29 (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 "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "Ga")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "Ga")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Var "Ga"))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) "holds"  (Bool  "("  (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "Ga"))))  ")" ))))) ; 
 
theorem :: TOPDIM_1:30 (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 "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "Ga")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "G")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Var "Ga"))  ($#r1_hidden :::"="::: )  (Set (Var "G")))) "holds"  (Bool  "("  (Bool (Set (Var "Ga")) "is"   ($#v2_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topdim_1 :::"ind"::: )  (Set (Var "Ga"))))  ")" ))))) ; 
 begin  
theorem :: TOPDIM_1:31 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ) "iff" (Bool  "ex" (Set (Var "Bas")) "being"   ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "st"  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "Bas")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A"))) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "("  ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "n"))  ($#k5_real_1 :::"-"::: )  (Num 1)))  ")" )))  ")" ))) ; 
 
theorem :: TOPDIM_1:32 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v7_pre_topc :::"T_1"::: )  ) & (Bool  "("   "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "A9")) "," (Set (Var "B9")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "A9"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B9"))) & (Bool (Set (Set (Var "A9"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B9")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "A9"))) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "B9")))  ")" ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: TOPDIM_1:33 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"SetSequence":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "g")) ")" ))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k8_nat_1 :::"."::: )  (Set (Var "i")))  ($#r1_xboole_0 :::"misses"::: )  (Set (Set (Var "g"))  ($#k8_nat_1 :::"."::: )  (Set (Var "j"))))  ")" ) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "fn")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "fn"))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "i")) ")" ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  "}"  ) & (Bool (Set (Set (Var "g"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k7_subset_1 :::"\"::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "fn")) ")" )))  ")" ))  ")" )  ")" )))) ; 
 
theorem :: TOPDIM_1:34 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "T")) "is"   ($#v1_metrizts :::"Lindelof"::: )  )) "holds"  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool  "ex" (Set (Var "A9")) "," (Set (Var "B9")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "A9"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B9"))) & (Bool (Set (Set (Var "A9"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "B9")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "A9"))) & (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "B9")))  ")" )))) ; 
 
theorem :: TOPDIM_1:35 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v7_pre_topc :::"T_1"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v1_metrizts :::"Lindelof"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k1_struct_0 :::"{}"::: )  (Set (Var "T")))  ($#r2_metrizts :::"separates"::: )  (Set (Var "A")) "," (Set (Var "B"))))  ")" )) ; 
 
theorem :: TOPDIM_1:36 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "T")) "is"   ($#v12_pre_topc :::"T_4"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v1_metrizts :::"Lindelof"::: )  ) & (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v2_tops_2 :::"closed"::: )  ) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (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   ($#k6_numbers :::"0"::: )  ))  ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v3_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k4_topdim_1 :::"ind"::: )  (Set (Var "T")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 



theorem :: TOPDIM_1:37 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "B")))) "holds"  (Bool  "for" (Set (Var "Null")) "being"   ($#v1_topdim_1 :::"finite-ind"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Null")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Null"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) "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 (Var "L"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Null")))  ")" ))))) ; 
 
theorem :: TOPDIM_1:38 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Null")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Null"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "Null")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Null")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "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 (Var "Null"))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "W"))))  ")" ))))  ")" ))) ; 
 
theorem :: TOPDIM_1:39 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Null")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Null"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  )) "holds"  (Bool  "("  (Bool  "("  (Bool (Set (Var "Null")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Null")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ) "iff" (Bool  "ex" (Set (Var "B")) "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 "B")))) "holds"  (Bool (Set (Var "Null"))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_tops_1 :::"Fr"::: )  (Set (Var "A"))))))  ")" ))) ; 
 
theorem :: TOPDIM_1:40 (Bool  "for" (Set (Var "TM")) "being"   ($#v3_pcomps_1 :::"metrizable"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Null")) "," (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TM"))  "st" (Bool (Bool (Set (Set (Var "TM"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "Null"))) "is"   ($#v5_waybel23 :::"second-countable"::: )  ) & (Bool (Set (Var "Null")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set (Var "A")) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set (Var "Null")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Null"))) "is"   ($#v1_topdim_1 :::"finite-ind"::: )  ) & (Bool (Set   ($#k2_topdim_1 :::"ind"::: )  (Set  "(" (Set (Var "A"))  ($#k4_subset_1 :::"\/"::: )  (Set (Var "Null")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k2_topdim_1 :::"ind"::: )  (Set (Var "A")) ")" )  ($#k3_real_1 :::"+"::: )  (Num 1)))  ")" ))) ;