:: T_0TOPSP  semantic presentation begin  
theorem :: T_0TOPSP:1 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool  "("   "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "x1"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x2"))))) "holds"  (Bool (Set (Var "x2"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))))) ; 
 definitionlet "T", "S" be    ($#l1_pre_topc :::"TopStruct"::: )  ; pred "T" "," "S" :::"are_homeomorphic":::  means :: T_0TOPSP:def 1 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "T" "," "S" "st" (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )); end; 





:: deftheorem    defines :::"are_homeomorphic"::: T_0TOPSP:def 1 :  (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "T")) "," (Set (Var "S"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st" (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ))  ")" )); 
 definitionlet "T", "S" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); attr "f" is  :::"open":::  means :: T_0TOPSP:def 2 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T"  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool (Set "f"  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))) "is"   ($#v3_pre_topc :::"open"::: )  )); end; 






:: deftheorem    defines :::"open"::: T_0TOPSP:def 2 :  (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_t_0topsp :::"open"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "A"))) "is"   ($#v3_pre_topc :::"open"::: )  ))  ")" ))); 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"Indiscernibility"::: "T" ->   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") means :: T_0TOPSP:def 3 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" "T" "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T"  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) "iff" (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" ))  ")" )); end; 





:: deftheorem    defines :::"Indiscernibility"::: T_0TOPSP:def 3 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_t_0topsp :::"Indiscernibility"::: )  (Set (Var "T")))) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) "iff" (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" ))  ")" ))  ")" ))); 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )  ; func  :::"Indiscernible"::: "T" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") equals :: T_0TOPSP:def 4 (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set  "("  ($#k1_t_0topsp :::"Indiscernibility"::: )  "T" ")" )); end; 





:: deftheorem    defines :::"Indiscernible"::: T_0TOPSP:def 4 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool (Set   ($#k2_t_0topsp :::"Indiscernible"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set  "("  ($#k1_t_0topsp :::"Indiscernibility"::: )  (Set (Var "T")) ")" )))); 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"T_0-reflex"::: "T" ->   ($#l1_pre_topc :::"TopSpace":::) equals :: T_0TOPSP:def 5 (Set   ($#k11_borsuk_1 :::"space"::: )  (Set  "("  ($#k2_t_0topsp :::"Indiscernible"::: )  "T" ")" )); end; 





:: deftheorem    defines :::"T_0-reflex"::: T_0TOPSP:def 5 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k3_t_0topsp :::"T_0-reflex"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_borsuk_1 :::"space"::: )  (Set  "("  ($#k2_t_0topsp :::"Indiscernible"::: )  (Set (Var "T")) ")" )))); 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k3_t_0topsp :::"T_0-reflex"::: )  "T") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  ; 
end; definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"T_0-canonical_map"::: "T" ->   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set  "("  ($#k3_t_0topsp :::"T_0-reflex"::: )  "T" ")" ) equals :: T_0TOPSP:def 6 (Set   ($#k12_borsuk_1 :::"Proj"::: )  (Set  "("  ($#k2_t_0topsp :::"Indiscernible"::: )  "T" ")" )); end; 





:: deftheorem    defines :::"T_0-canonical_map"::: T_0TOPSP:def 6 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_borsuk_1 :::"Proj"::: )  (Set  "("  ($#k2_t_0topsp :::"Indiscernible"::: )  (Set (Var "T")) ")" )))); 
 
theorem :: T_0TOPSP:2 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_t_0topsp :::"T_0-reflex"::: )  (Set (Var "T")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "V")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "V")))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))))  ")" ))) ; 
 
theorem :: T_0TOPSP:3 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "C")) "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k3_t_0topsp :::"T_0-reflex"::: )  (Set (Var "T")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Set (Var "C"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k1_t_0topsp :::"Indiscernibility"::: )  (Set (Var "T")) ")" ) "," (Set (Var "p")) ")" )))  ")" ))) ; 
 
theorem :: T_0TOPSP:4 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set  "("  ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k1_t_0topsp :::"Indiscernibility"::: )  (Set (Var "T")) ")" ) "," (Set (Var "p")) ")" )))) ; 
 
theorem :: T_0TOPSP:5 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))) "iff" (Bool (Set  ($#k4_borsuk_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "p")) ($#k4_borsuk_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_t_0topsp :::"Indiscernibility"::: )  (Set (Var "T"))))  ")" ))) ; 
 
theorem :: T_0TOPSP:6 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#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"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Set  "("  ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))))) ; 
 
theorem :: T_0TOPSP:7 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#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"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_t_0topsp :::"Indiscernible"::: )  (Set (Var "T")))) & (Bool (Set (Var "C"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))))) ; 
 
theorem :: T_0TOPSP:8 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T"))) "is"   ($#v1_t_0topsp :::"open"::: )  )) ; 
 definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; redefine attr "T" is  :::"T_0":::  means :: T_0TOPSP:def 7 (Bool  "("  (Bool "T" "is"   ($#v2_struct_0 :::"empty"::: )  ) "or" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" "T"  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "T" "st"  (Bool  "("  (Bool (Set (Var "V")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))))  ")" )  ")" )  ")" )))  ")" ); end; 




:: deftheorem    defines :::"T_0"::: T_0TOPSP:def 7 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v6_pre_topc :::"T_0"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v2_struct_0 :::"empty"::: )  ) "or" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool  "ex" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "V")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))))  ")" ) "or" (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "V"))))  ")" )  ")" )  ")" )))  ")" )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v6_pre_topc :::"T_0"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; definitionmode T_0-TopSpace is  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_pre_topc :::"T_0"::: )    ($#l1_pre_topc :::"TopSpace":::); end; 
theorem :: T_0TOPSP:9 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k3_t_0topsp :::"T_0-reflex"::: )  (Set (Var "T"))) "is"   ($#l1_pre_topc :::"T_0-TopSpace":::))) ; 
 
theorem :: T_0TOPSP:10 (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_t_0topsp :::"T_0-reflex"::: )  (Set (Var "S")) ")" ) "," (Set  "("  ($#k3_t_0topsp :::"T_0-reflex"::: )  (Set (Var "T")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "h")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set   ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T"))) "," (Set (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "S")) ")" ))  ($#r2_classes1 :::"are_fiberwise_equipotent"::: )  )  ")" ))) "holds"  (Bool (Set (Var "T")) "," (Set (Var "S"))  ($#r1_t_0topsp :::"are_homeomorphic"::: )  )) ; 
 
theorem :: T_0TOPSP:11 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T0")) "being"   ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T0"))  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set  ($#k4_borsuk_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_borsuk_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_t_0topsp :::"Indiscernibility"::: )  (Set (Var "T"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "q")))))))) ; 
 
theorem :: T_0TOPSP:12 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T0")) "being"   ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T0"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k1_t_0topsp :::"Indiscernibility"::: )  (Set (Var "T")) ")" ) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" ) ($#k1_tarski :::"}"::: ) )))))) ; 
 
theorem :: T_0TOPSP:13 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T0")) "being"   ($#l1_pre_topc :::"T_0-TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T0")) (Bool  "ex" (Set (Var "h")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_t_0topsp :::"T_0-reflex"::: )  (Set (Var "T")) ")" ) "," (Set (Var "T0")) "st" (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k4_t_0topsp :::"T_0-canonical_map"::: )  (Set (Var "T")) ")" ))))))) ;