:: BORSUK_3  semantic presentation begin  
theorem :: BORSUK_3:1 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "S")) ")" ) "," (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")) ")" ) ($#k3_borsuk_1 :::":]"::: ) ))) ; 
 
theorem :: BORSUK_3:2 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Set (Var "Y"))  ($#k6_struct_0 :::"-->"::: )  (Set (Var "x"))) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" )))) ; 
 registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster (Set   ($#k3_struct_0 :::"id"::: )  "T") ->   ($#v3_tops_2 :::"being_homeomorphism"::: )   ; 
end; definitionlet "S", "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; :: original: :::"are_homeomorphic"::: redefine pred "S" "," "T" :::"are_homeomorphic"::: ; reflexivity  
(Bool  "for" (Set (Var "S")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool bbbadR1_T_0TOPSP((Set (Var "b1")) "," (Set (Var "b1")))))
 ; end; definitionlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )  ; :: original: :::"are_homeomorphic"::: redefine pred "S" "," "T" :::"are_homeomorphic"::: ; reflexivity  
(Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )   "holds"  (Bool bbbadR1_T_0TOPSP((Set (Var "b1")) "," (Set (Var "b1")))))
 ; symmetry  
(Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    "st" (Bool (Bool bbbadR1_T_0TOPSP((Set (Var "b1")) "," (Set (Var "b2"))))) "holds"  (Bool bbbadR1_T_0TOPSP((Set (Var "b2")) "," (Set (Var "b1")))))
 ; end; 
theorem :: BORSUK_3:3 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  ) & (Bool (Set (Var "T")) "," (Set (Var "V"))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set (Var "S")) "," (Set (Var "V"))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  )) ; 
 begin  registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "P" be   ($#v1_xboole_0 :::"empty"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "P") ->   ($#v2_struct_0 :::"empty"::: )   ; 
end; registration
cluster   ($#v2_struct_0 :::"empty"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    ->   ($#v1_compts_1 :::"compact"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; 
theorem :: BORSUK_3:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )))) ; 
 
theorem :: BORSUK_3:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k10_funct_3 :::"pr2"::: )   "(" (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )))) ; 
 
theorem :: BORSUK_3:6 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"""::: )  )  ($#r1_funct_2 :::"="::: )  (Set  ($#k14_funct_3 :::"<:"::: ) (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "Y")) ")" ) "," (Set  "(" (Set (Var "Y"))  ($#k6_struct_0 :::"-->"::: )  (Set (Var "x")) ")" ) ($#k14_funct_3 :::":>"::: ) ))))) ; 
 
theorem :: BORSUK_3:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k10_funct_3 :::"pr2"::: )   "(" (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"""::: )  )  ($#r1_funct_2 :::"="::: )  (Set  ($#k14_funct_3 :::"<:"::: ) (Set  "(" (Set (Var "Y"))  ($#k6_struct_0 :::"-->"::: )  (Set (Var "x")) ")" ) "," (Set  "("  ($#k3_struct_0 :::"id"::: )  (Set (Var "Y")) ")" ) ($#k14_funct_3 :::":>"::: ) ))))) ; 
 
theorem :: BORSUK_3:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k9_funct_3 :::"pr1"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )))) ; 
 
theorem :: BORSUK_3:9 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_funct_2 :::"="::: )  (Set   ($#k10_funct_3 :::"pr2"::: )   "(" (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ")" ))) "holds"  (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )))) ; 
 begin  
theorem :: BORSUK_3:10 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "G")))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))) "st"  (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "Y"))))) "holds"  (Bool  "ex" (Set (Var "G1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))(Bool  "ex" (Set (Var "H1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "G1")) "," (Set (Var "H1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "i")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "G1")) "," (Set (Var "H1")) ($#k3_borsuk_1 :::":]"::: ) )) & (Bool (Set (Var "G1")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set (Var "H1")) "is"   ($#v3_pre_topc :::"open"::: )  ) & (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "G1")) "," (Set (Var "H1")) ($#k3_borsuk_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "G")))  ")" ))))))))) ; 
 
theorem :: BORSUK_3:11 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")) ")" ) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "G")))) "holds"  (Bool  "ex" (Set (Var "R")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "R"))) & (Bool (Set (Var "R"))  ($#r1_tarski :::"c="::: )   "{"  (Set (Var "y")) where y "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")) ")" ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_borsuk_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "G")))  "}"  )  ")" )))))) ; 
 
theorem :: BORSUK_3:12 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "G")) "being"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) ) "holds"  (Bool  "{"  (Set (Var "x")) where x "is"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) : (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")) ")" ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_borsuk_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "G")))  "}"    ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "X"))))))) ; 
 
theorem :: BORSUK_3:13 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  ))) ; 
 
theorem :: BORSUK_3:14 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  ) & (Bool (Set (Var "S")) "is"   ($#v1_compts_1 :::"compact"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_compts_1 :::"compact"::: )  )) ; 
 
theorem :: BORSUK_3:15 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "XV")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "XV")) ($#k2_borsuk_1 :::":]"::: ) ) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )))) ; 
 
theorem :: BORSUK_3:16 (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")) ")" ) "," (Set  ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) ($#k3_borsuk_1 :::":]"::: ) ))) "holds"  (Bool (Set (Var "Z")) "is"   ($#v2_compts_1 :::"compact"::: )  ))))) ; 
 registrationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "Y" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::); let "x" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "Y" "," (Set  "(" "X"  ($#k1_pre_topc :::"|"::: )  (Set  ($#k6_domain_1 :::"{"::: ) "x" ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v1_compts_1 :::"compact"::: )   ; 
end; 
theorem :: BORSUK_3:17 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "Q")) where Q "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "Q")) ($#k3_borsuk_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "("  ($#k7_borsuk_1 :::"Base-Appr"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) ) ")" ) ")" )))  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "R")) "is"    ($#m1_setfam_1 :::"Cover"::: )   "of" (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "X"))))  ")" ))) ; 
 
theorem :: BORSUK_3:18 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "Q")) where Q "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "ex" (Set (Var "FQ")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "FQ"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "FQ")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "Q")) ($#k3_borsuk_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "FQ"))))  ")" ))  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "R")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "R")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "X")))  ")" )))) ; 
 
theorem :: BORSUK_3:19 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "R")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  ) & (Bool (Set (Var "R"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "Q")) where Q "is"   ($#v3_pre_topc :::"open"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool  "ex" (Set (Var "FQ")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "FQ"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "FQ")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "Q")) ($#k3_borsuk_1 :::":]"::: ) )  ($#r1_tarski :::"c="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set (Var "FQ"))))  ")" ))  "}"  )) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "R"))) & (Bool (Set (Var "C")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "C")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "X")))  ")" ))))) ; 
 
theorem :: BORSUK_3:20 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  )) "holds"  (Bool  "ex" (Set (Var "G")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) ) "st"  (Bool  "("  (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "F"))) & (Bool (Set (Var "G")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )) & (Bool (Set (Var "G")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )))) ; 
 registrationlet "T1", "T2" be   ($#v1_compts_1 :::"compact"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "T1" "," "T2" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v1_compts_1 :::"compact"::: )   ; 
end; 
theorem :: BORSUK_3:21 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "XV")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "YV")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "Y")) "holds"  (Bool (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "XV")) "," (Set (Var "YV")) ($#k2_borsuk_1 :::":]"::: ) ) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ))))) ; 
 
theorem :: BORSUK_3:22 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "Z")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  (Bool  "for" (Set (Var "V")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "W")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "Z"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "W")) "," (Set (Var "V")) ($#k3_borsuk_1 :::":]"::: ) ))) "holds"  (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "(" (Set (Var "Y"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "W")) ")" ) "," (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "V")) ")" ) ($#k2_borsuk_1 :::":]"::: ) )) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "(" (Set (Var "Y"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "W")) ")" ) "," (Set  "(" (Set (Var "X"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "V")) ")" ) ($#k2_borsuk_1 :::":]"::: ) )) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "Z")) ")" )) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  "(" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_borsuk_1 :::":]"::: ) )  ($#k1_pre_topc :::"|"::: )  (Set (Var "Z")) ")" )) "#)" )))))) ; 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster   ($#v1_xboole_0 :::"empty"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")); 
end; registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); let "P" be   ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k1_pre_topc :::"|"::: )  "P") ->   ($#v1_compts_1 :::"compact"::: )   ; 
end; 
theorem :: BORSUK_3:23 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "S1")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T1"))  (Bool  "for" (Set (Var "S2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T2"))  "st" (Bool (Bool (Set (Var "S1")) "is"   ($#v2_compts_1 :::"compact"::: )  ) & (Bool (Set (Var "S2")) "is"   ($#v2_compts_1 :::"compact"::: )  )) "holds"  (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "S1")) "," (Set (Var "S2")) ($#k3_borsuk_1 :::":]"::: ) ) "is"   ($#v2_compts_1 :::"compact"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ))))) ;