:: T_1TOPSP  semantic presentation begin  




theorem :: T_1TOPSP:1 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  (Bool  "for" (Set (Var "y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k11_borsuk_1 :::"space"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k12_borsuk_1 :::"Proj"::: )  (Set (Var "A")) ")" )  ($#k8_relset_1 :::"""::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "y"))))))) ; 
 
theorem :: T_1TOPSP:2 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k11_borsuk_1 :::"space"::: )  (Set (Var "S")) ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool (Set (Var "B")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" ))))) ; 
 



theorem :: T_1TOPSP:3 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool  "{"  (Set (Var "A")) where A "is"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) : (Bool (Set (Var "A")) "is"   ($#v2_tops_2 :::"closed"::: )  )  "}"   "is"   ($#m1_subset_1 :::"Part-Family":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))))) ; 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"Closed_Partitions"::: "T" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Part-Family":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") equals :: T_1TOPSP:def 1  "{"  (Set (Var "A")) where A "is"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") : (Bool (Set (Var "A")) "is"   ($#v2_tops_2 :::"closed"::: )  )  "}"  ; end; 





:: deftheorem    defines :::"Closed_Partitions"::: T_1TOPSP:def 1 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k1_t_1topsp :::"Closed_Partitions"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "A")) where A "is"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) : (Bool (Set (Var "A")) "is"   ($#v2_tops_2 :::"closed"::: )  )  "}"  )); 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"T_1-reflex"::: "T" ->   ($#l1_pre_topc :::"TopSpace":::) equals :: T_1TOPSP:def 2 (Set   ($#k11_borsuk_1 :::"space"::: )  (Set  "("  ($#k12_eqrel_1 :::"Intersection"::: )  (Set  "("  ($#k1_t_1topsp :::"Closed_Partitions"::: )  "T" ")" ) ")" )); end; 





:: deftheorem    defines :::"T_1-reflex"::: T_1TOPSP:def 2 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_t_1topsp :::"T_1-reflex"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_borsuk_1 :::"space"::: )  (Set  "("  ($#k12_eqrel_1 :::"Intersection"::: )  (Set  "("  ($#k1_t_1topsp :::"Closed_Partitions"::: )  (Set (Var "T")) ")" ) ")" )))); 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k2_t_1topsp :::"T_1-reflex"::: )  "T") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )   ; 
end; 
theorem :: T_1TOPSP:4 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_t_1topsp :::"T_1-reflex"::: )  (Set (Var "T"))) "is"   ($#v7_pre_topc :::"T_1"::: )  )) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#k2_t_1topsp :::"T_1-reflex"::: )  "T") ->   ($#v7_pre_topc :::"T_1"::: )   ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v7_pre_topc :::"T_1"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); func  :::"T_1-reflect"::: "T" ->   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" "T" "," (Set  "("  ($#k2_t_1topsp :::"T_1-reflex"::: )  "T" ")" ) equals :: T_1TOPSP:def 3 (Set   ($#k12_borsuk_1 :::"Proj"::: )  (Set  "("  ($#k12_eqrel_1 :::"Intersection"::: )  (Set  "("  ($#k1_t_1topsp :::"Closed_Partitions"::: )  "T" ")" ) ")" )); end; 





:: deftheorem    defines :::"T_1-reflect"::: T_1TOPSP:def 3 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k3_t_1topsp :::"T_1-reflect"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_borsuk_1 :::"Proj"::: )  (Set  "("  ($#k12_eqrel_1 :::"Intersection"::: )  (Set  "("  ($#k1_t_1topsp :::"Closed_Partitions"::: )  (Set (Var "T")) ")" ) ")" )))); 
 
theorem :: T_1TOPSP:5 (Bool  "for" (Set (Var "T")) "," (Set (Var "T1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T1"))  "st" (Bool (Bool (Set (Var "T1")) "is"   ($#v7_pre_topc :::"T_1"::: )  )) "holds"  (Bool  "("  (Bool  "{"  (Set  "(" (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "z")) ($#k6_domain_1 :::"}"::: ) ) ")" ) where z "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T1")) : (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f"))))  "}"   "is"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T")))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )   "{"  (Set  "(" (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "z")) ($#k6_domain_1 :::"}"::: ) ) ")" ) where z "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T1")) : (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f"))))  "}"  )) "holds"  (Bool (Set (Var "A")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )  ")" ))) ; 
 
theorem :: T_1TOPSP:6 (Bool  "for" (Set (Var "T")) "," (Set (Var "T1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T1"))  "st" (Bool (Bool (Set (Var "T1")) "is"   ($#v7_pre_topc :::"T_1"::: )  )) "holds"  (Bool  "for" (Set (Var "w")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "w"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_eqrel_1 :::"EqClass"::: )   "(" (Set (Var "x")) "," (Set  "("  ($#k12_eqrel_1 :::"Intersection"::: )  (Set  "("  ($#k1_t_1topsp :::"Closed_Partitions"::: )  (Set (Var "T")) ")" ) ")" ) ")" ))) "holds"  (Bool (Set (Var "w"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")) ")" ) ($#k6_domain_1 :::"}"::: ) ))))))) ; 
 
theorem :: T_1TOPSP:7 (Bool  "for" (Set (Var "T")) "," (Set (Var "T1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T1"))  "st" (Bool (Bool (Set (Var "T1")) "is"   ($#v7_pre_topc :::"T_1"::: )  )) "holds"  (Bool  "for" (Set (Var "w")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k2_t_1topsp :::"T_1-reflex"::: )  (Set (Var "T")) ")" )))) "holds"  (Bool  "ex" (Set (Var "z")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T1")) "st"  (Bool  "("  (Bool (Set (Var "z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set (Var "w"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "z")) ($#k6_domain_1 :::"}"::: ) )))  ")" ))))) ; 
 
theorem :: T_1TOPSP:8 (Bool  "for" (Set (Var "T")) "," (Set (Var "T1")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "T1"))  "st" (Bool (Bool (Set (Var "T1")) "is"   ($#v7_pre_topc :::"T_1"::: )  )) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_t_1topsp :::"T_1-reflex"::: )  (Set (Var "T")) ")" ) "," (Set (Var "T1")) "st" (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "h"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k3_t_1topsp :::"T_1-reflect"::: )  (Set (Var "T")) ")" )))))) ; 
 definitionlet "T", "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "f" be   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); func  :::"T_1-reflex"::: "f" ->   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_t_1topsp :::"T_1-reflex"::: )  "T" ")" ) "," (Set  "("  ($#k2_t_1topsp :::"T_1-reflex"::: )  "S" ")" ) means :: T_1TOPSP:def 4 (Bool (Set (Set  "("  ($#k3_t_1topsp :::"T_1-reflect"::: )  "S" ")" )  ($#k1_partfun1 :::"*"::: )  "f")  ($#r2_funct_2 :::"="::: )  (Set it  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k3_t_1topsp :::"T_1-reflect"::: )  "T" ")" ))); end; 







:: deftheorem    defines :::"T_1-reflex"::: T_1TOPSP:def 4 :  (Bool  "for" (Set (Var "T")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "b4")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_t_1topsp :::"T_1-reflex"::: )  (Set (Var "T")) ")" ) "," (Set  "("  ($#k2_t_1topsp :::"T_1-reflex"::: )  (Set (Var "S")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_t_1topsp :::"T_1-reflex"::: )  (Set (Var "f")))) "iff" (Bool (Set (Set  "("  ($#k3_t_1topsp :::"T_1-reflect"::: )  (Set (Var "S")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set (Var "f")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "b4"))  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k3_t_1topsp :::"T_1-reflect"::: )  (Set (Var "T")) ")" )))  ")" ))));