:: BORSUK_2  semantic presentation begin  





scheme  :: BORSUK_2:sch 1 FrCard{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set F3 "(" (Set (Var "w")) ")" ) where w "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool  "("  (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" )) & (Bool P1[(Set (Var "w"))])  ")" )  "}"  )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set F2 "("  ")" )))
 proof 


end; 
theorem :: BORSUK_2:1 (Bool  "for" (Set (Var "T1")) "," (Set (Var "S")) "," (Set (Var "T2")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T1")) "," (Set (Var "S"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T2")) "," (Set (Var "S"))  "st" (Bool (Bool (Set (Var "T1")) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))) & (Bool (Set (Var "T2")) "is"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set (Var "T"))) & (Bool (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T")))) & (Bool (Set (Var "T1")) "is"   ($#v1_compts_1 :::"compact"::: )  ) & (Bool (Set (Var "T2")) "is"   ($#v1_compts_1 :::"compact"::: )  ) & (Bool (Set (Var "T")) "is"   ($#v8_pre_topc :::"T_2"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")))) & (Bool (Set (Var "h")) "is"   ($#v5_pre_topc :::"continuous"::: )  )  ")" ))))) ; 
 registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster (Set   ($#k3_struct_0 :::"id"::: )  "T") ->   ($#v5_pre_topc :::"continuous"::: )     ($#v1_t_0topsp :::"open"::: )   ; 
end; registrationlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v2_funct_1 :::"one-to-one"::: )   bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")) bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))   ($#v5_pre_topc :::"continuous"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 
theorem :: BORSUK_2:2 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tops_2 :::"""::: )  ) "is"   ($#v1_t_0topsp :::"open"::: )  ))) ; 
 begin  
theorem :: BORSUK_2:3 (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 :::"Point":::) "of" (Set (Var "T")) (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )))) ; 
 definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); pred "a" "," "b" :::"are_connected":::  means :: BORSUK_2:def 1 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," "T" "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  "a") & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "b")  ")" )); end; 






:: deftheorem    defines :::"are_connected"::: BORSUK_2:def 1 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_borsuk_2 :::"are_connected"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))  ")" ))); 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); :: original: :::"are_connected"::: redefine pred "a" "," "b" :::"are_connected"::: ; reflexivity  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")) "holds"  (Bool ((Set (Const "T")) "," (Set (Var "b1")) "," (Set (Var "b1")))))
 ; end; definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); assume 
(Bool (Set (Const "a")) "," (Set (Const "b"))  ($#r1_borsuk_2 :::"are_connected"::: )  )
 ; mode  :::"Path":::  "of" "a" "," "b" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," "T" means :: BORSUK_2:def 2 (Bool  "("  (Bool it "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  "a") & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "b")  ")" ); end; 








:: deftheorem    defines :::"Path"::: BORSUK_2:def 2 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_borsuk_2 :::"are_connected"::: )  )) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "b4")) "is"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool  "("  (Bool (Set (Var "b4")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )  ")" )))); 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ))  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ))) bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))   ($#v5_pre_topc :::"continuous"::: )    for    ($#m1_borsuk_2 :::"Path"::: )   "of" "a" "," "a"; 
end; definitionlet "T" be    ($#l1_pre_topc :::"TopStruct"::: )  ; attr "T" is  :::"pathwise_connected":::  means :: BORSUK_2:def 3 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" "T" "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_borsuk_2 :::"are_connected"::: )  )); end; 




:: deftheorem    defines :::"pathwise_connected"::: BORSUK_2:def 3 :  (Bool  "for" (Set (Var "T")) "being"    ($#l1_pre_topc :::"TopStruct"::: )   "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v1_borsuk_2 :::"pathwise_connected"::: )  ) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_borsuk_2 :::"are_connected"::: )  ))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_pre_topc :::"strict"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v1_borsuk_2 :::"pathwise_connected"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; definitionlet "T" be   ($#v1_borsuk_2 :::"pathwise_connected"::: )     ($#l1_pre_topc :::"TopStruct"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); redefine mode  :::"Path":::  "of" "a" "," "b" means :: BORSUK_2:def 4 (Bool  "("  (Bool it "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  "a") & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "b")  ")" ); end; 







:: deftheorem    defines :::"Path"::: BORSUK_2:def 4 :  (Bool  "for" (Set (Var "T")) "being"   ($#v1_borsuk_2 :::"pathwise_connected"::: )     ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) "holds"   (Bool  "("  (Bool (Set (Var "b4")) "is"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool  "("  (Bool (Set (Var "b4")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )  ")" )))); 
 registrationlet "T" be   ($#v1_borsuk_2 :::"pathwise_connected"::: )     ($#l1_pre_topc :::"TopStruct"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster   ->   ($#v5_pre_topc :::"continuous"::: )    for    ($#m1_borsuk_2 :::"Path"::: )   "of" "a" "," "b"; 
end; 






registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_pre_topc :::"TopSpace-like"::: )     ($#v1_borsuk_2 :::"pathwise_connected"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_connsp_1 :::"connected"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; begin  definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a", "b", "c" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "b")); let "Q" be    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "b")) "," (Set (Const "c")); assume that  
(Bool (Set (Const "a")) "," (Set (Const "b"))  ($#r2_borsuk_2 :::"are_connected"::: )  )
 and  
(Bool (Set (Const "b")) "," (Set (Const "c"))  ($#r2_borsuk_2 :::"are_connected"::: )  )
 ; func "P" :::"+"::: "Q" ->    ($#m1_borsuk_2 :::"Path"::: )   "of" "a" "," "c" means :: BORSUK_2:def 5 (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2)))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set "P"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t")))) "implies" (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set "Q"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )))  ")"   ")" )); end; 











:: deftheorem    defines :::"+"::: BORSUK_2:def 5 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "Q")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "b")) "," (Set (Var "c"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_borsuk_2 :::"are_connected"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r2_borsuk_2 :::"are_connected"::: )  )) "holds"  (Bool  "for" (Set (Var "b7")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "c")) "holds"   (Bool  "("  (Bool (Set (Var "b7"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k1_borsuk_2 :::"+"::: )  (Set (Var "Q")))) "iff" (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "t"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2)))) "implies" (Bool (Set (Set (Var "b7"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" )))  ")"  &  "("  (Bool (Bool (Set (Num 1)  ($#k10_real_1 :::"/"::: )  (Num 2))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "t")))) "implies" (Bool (Set (Set (Var "b7"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Q"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "t")) ")" )  ($#k9_real_1 :::"-"::: )  (Num 1) ")" )))  ")"   ")" ))  ")" )))))); 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ))  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_funct_1 :::"constant"::: )   bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ))) bbbadV1_FUNCT_2((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k5_topmetr :::"I[01]"::: ) )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T"))  for    ($#m1_borsuk_2 :::"Path"::: )   "of" "a" "," "a"; 
end; 
theorem :: BORSUK_2:4 canceled; 
 
theorem :: BORSUK_2:5 (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 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"   ($#v3_funct_1 :::"constant"::: )     ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "a")) "holds"  (Bool (Set (Var "P"))  ($#r2_funct_2 :::"="::: )  (Set (Set  ($#k5_topmetr :::"I[01]"::: ) )  ($#k6_struct_0 :::"-->"::: )  (Set (Var "a"))))))) ; 
 
theorem :: BORSUK_2: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 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"   ($#v3_funct_1 :::"constant"::: )     ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "a")) "holds"  (Bool (Set (Set (Var "P"))  ($#k1_borsuk_2 :::"+"::: )  (Set (Var "P")))  ($#r2_funct_2 :::"="::: )  (Set (Var "P")))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be   ($#v3_funct_1 :::"constant"::: )     ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "a")); 
cluster (Set "P"  ($#k1_borsuk_2 :::"+"::: )  "P") ->   ($#v3_funct_1 :::"constant"::: )   ; 
end; definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "b")); assume 
(Bool (Set (Const "a")) "," (Set (Const "b"))  ($#r2_borsuk_2 :::"are_connected"::: )  )
 ; func  :::"-"::: "P" ->    ($#m1_borsuk_2 :::"Path"::: )   "of" "b" "," "a" means :: BORSUK_2:def 6 (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set "P"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "t")) ")" )))); end; 









:: deftheorem    defines :::"-"::: BORSUK_2:def 6 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_borsuk_2 :::"are_connected"::: )  )) "holds"  (Bool  "for" (Set (Var "b5")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "b")) "," (Set (Var "a")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_borsuk_2 :::"-"::: )  (Set (Var "P")))) "iff" (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"  (Bool (Set (Set (Var "b5"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Num 1)  ($#k9_real_1 :::"-"::: )  (Set (Var "t")) ")" ))))  ")" ))))); 
 
theorem :: BORSUK_2: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 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"   ($#v3_funct_1 :::"constant"::: )     ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "a")) "holds"  (Bool (Set   ($#k2_borsuk_2 :::"-"::: )  (Set (Var "P")))  ($#r2_funct_2 :::"="::: )  (Set (Var "P")))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be   ($#v3_funct_1 :::"constant"::: )     ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "a")); 
cluster (Set   ($#k2_borsuk_2 :::"-"::: )  "P") ->   ($#v3_funct_1 :::"constant"::: )   ; 
end; begin  
theorem :: BORSUK_2: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 "A")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  "("  ($#k5_setfam_1 :::"union"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_setfam_1 :::"union"::: )  (Set  "(" (Set (Var "f"))  ($#k6_funct_2 :::"""::: )  (Set (Var "A")) ")" )))))) ; 
 definitionlet "S1", "S2", "T1", "T2" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S1")) "," (Set (Const "S2")); let "g" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T1")) "," (Set (Const "T2")); :: original: :::"[:"::: redefine func :::"[:":::"f" "," "g":::":]"::: ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) "S1" "," "T1" ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) "S2" "," "T2" ($#k2_borsuk_1 :::":]"::: ) ); end; 
theorem :: BORSUK_2:9 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "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 "S1")) "," (Set (Var "T1"))  (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S2")) "," (Set (Var "T2"))  (Bool  "for" (Set (Var "P1")) "," (Set (Var "P2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "P2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_borsuk_1 :::"Base-Appr"::: )  (Set (Var "P1"))))) "holds"  (Bool (Set (Set  ($#k3_borsuk_2 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_borsuk_2 :::":]"::: ) )  ($#k8_relset_1 :::"""::: )  (Set (Var "P2"))) "is"   ($#v3_pre_topc :::"open"::: )  ))))) ; 
 
theorem :: BORSUK_2:10 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "T1")) "," (Set (Var "T2")) "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 "S1")) "," (Set (Var "T1"))  (Bool  "for" (Set (Var "g")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S2")) "," (Set (Var "T2"))  (Bool  "for" (Set (Var "P2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) )  "st" (Bool (Bool (Set (Var "P2")) "is"   ($#v3_pre_topc :::"open"::: )  )) "holds"  (Bool (Set (Set  ($#k3_borsuk_2 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_borsuk_2 :::":]"::: ) )  ($#k8_relset_1 :::"""::: )  (Set (Var "P2"))) "is"   ($#v3_pre_topc :::"open"::: )  ))))) ; 
 registrationlet "S1", "S2", "T1", "T2" 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 "S1")) "," (Set (Const "T1")); let "g" be   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S2")) "," (Set (Const "T2")); 
cluster (Set  ($#k15_funct_3 :::"[:"::: ) "f" "," "g" ($#k15_funct_3 :::":]"::: ) ) ->   ($#v5_pre_topc :::"continuous"::: )    for  ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) "S1" "," "S2" ($#k2_borsuk_1 :::":]"::: ) ) "," (Set  ($#k2_borsuk_1 :::"[:"::: ) "T1" "," "T2" ($#k2_borsuk_1 :::":]"::: ) ); 
end; registrationlet "T1", "T2" be   ($#v6_pre_topc :::"T_0"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "T1" "," "T2" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v6_pre_topc :::"T_0"::: )   ; 
end; registrationlet "T1", "T2" be   ($#v7_pre_topc :::"T_1"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "T1" "," "T2" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v7_pre_topc :::"T_1"::: )   ; 
end; registrationlet "T1", "T2" be   ($#v8_pre_topc :::"T_2"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "T1" "," "T2" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v8_pre_topc :::"T_2"::: )   ; 
end; registration
cluster (Set   ($#k17_borsuk_1 :::"I[01]"::: )  ) ->   ($#v8_pre_topc :::"T_2"::: )     ($#v1_compts_1 :::"compact"::: )   ; 
end; definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )  ; let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P", "Q" be    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "b")); pred "P" "," "Q" :::"are_homotopic":::  means :: BORSUK_2:def 7 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," "T" "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set "P"  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set "Q"  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  "a") & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Num 1) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  "b")  ")" )  ")" )  ")" )); symmetry  
(Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "b"))  "st" (Bool (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "T")) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Q"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set (Const "a"))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Num 1) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set (Const "b")))  ")" )  ")" )  ")" ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "T")) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Q"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set (Const "a"))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Num 1) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set (Const "b")))  ")" )  ")" )  ")" )))
 ; end; 








:: deftheorem    defines :::"are_homotopic"::: BORSUK_2:def 7 :  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b")) "holds"   (Bool  "("  (Bool (Set (Var "P")) "," (Set (Var "Q"))  ($#r3_borsuk_2 :::"are_homotopic"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set  ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool  "("   "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "P"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set (Var "t")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "Q"))  ($#k3_funct_2 :::"."::: )  (Set (Var "t")))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "f"))  ($#k1_binop_1 :::"."::: )   "(" (Num 1) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" )  ")" )  ")" ))  ")" )))); 
 
theorem :: BORSUK_2:11 canceled; 
 
theorem :: BORSUK_2:12 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r2_borsuk_2 :::"are_connected"::: )  )) "holds"  (Bool (Set (Var "P")) "," (Set (Var "P"))  ($#r3_borsuk_2 :::"are_homotopic"::: )  )))) ; 
 definitionlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_borsuk_2 :::"pathwise_connected"::: )    ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P", "Q" be    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "b")); :: original: :::"are_homotopic"::: redefine pred "P" "," "Q" :::"are_homotopic"::: ; reflexivity  
(Bool  "for" (Set (Var "P")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "b")) "holds"  (Bool ((Set (Const "T")) "," (Set (Const "a")) "," (Set (Const "b")) "," (Set (Var "b1")) "," (Set (Var "b1")))))
 ; end; 
theorem :: BORSUK_2:13 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "w1")) "," (Set (Var "w2")) "," (Set (Var "w3")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "h1")) "," (Set (Var "h2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "G"))  "st" (Bool (Bool (Set (Var "h1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "w1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h1"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Var "h2")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "w2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h2"))  ($#k1_funct_1 :::"."::: )  (Num 1)))) "holds"  (Bool  "ex" (Set (Var "h3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "h3")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "w1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h3"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "w3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h3"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "h3")))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "h1")) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "("  ($#k2_relset_1 :::"rng"::: )  (Set (Var "h2")) ")" )))  ")" ))))) ; 
 
theorem :: BORSUK_2:14 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "G1")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "G2")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "b")) "," (Set (Var "c"))  "st" (Bool (Bool (Set (Var "G1")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Var "G2")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "G1"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "G1"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set (Var "G2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set (Var "G2"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "c")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "G1"))  ($#k1_borsuk_2 :::"+"::: )  (Set (Var "G2"))) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set  "(" (Set (Var "G1"))  ($#k1_borsuk_2 :::"+"::: )  (Set (Var "G2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set  "(" (Set (Var "G1"))  ($#k1_borsuk_2 :::"+"::: )  (Set (Var "G2")) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")" ))))) ; 
 registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_connsp_1 :::"connected"::: )     ($#v2_compts_1 :::"compact"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T")); 
end; 
theorem :: BORSUK_2:15 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")" ))) "holds"  (Bool  "ex" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )))) ; 
 registration
cluster (Set   ($#k17_borsuk_1 :::"I[01]"::: )  ) ->   ($#v1_borsuk_2 :::"pathwise_connected"::: )   ; 
end;