:: TOPALG_3  semantic presentation begin  
theorem :: TOPALG_3:1 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "a"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "b")) ")" )) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B"))))) ; 
 
theorem :: TOPALG_3:2 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k2_funct_1 :::"""::: )  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))))) ; 
 
theorem :: TOPALG_3:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" )  ($#k4_subset_1 :::"\/"::: )  (Set  "(" (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ) ")" ))))) ; 
 
theorem :: TOPALG_3:4 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_struct_0 :::"1-sorted"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds"  (Bool (Set (Set  "(" (Set (Var "S"))  ($#k6_struct_0 :::"-->"::: )  (Set (Var "t")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "t")))))) ; 
 
theorem :: TOPALG_3:5 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_pre_topc :::"TopStruct"::: )    (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "t")) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set   ($#k1_tex_2 :::"Sspace"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A"))))))) ; 
 
theorem :: TOPALG_3:6 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "C"))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Var "D")))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r1_connsp_1 :::"are_separated"::: )  ) "iff" (Bool (Set (Var "C")) "," (Set (Var "D"))  ($#r1_connsp_1 :::"are_separated"::: )  )  ")" )))) ; 
 
theorem :: TOPALG_3:7 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v1_connsp_1 :::"connected"::: )  ) "iff" (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set  "("  ($#k1_compts_1 :::"1TopSp"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ")" )  "holds"  (Bool  "("   "not" (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  ) "or"  "not" (Bool (Set (Var "f")) "is"   ($#v2_funct_2 :::"onto"::: )  )  ")" ))  ")" )) ; 
 registration
cluster   ($#v2_struct_0 :::"empty"::: )    ->   ($#v1_connsp_1 :::"connected"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; 
theorem :: TOPALG_3:8 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  "st" (Bool (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" ) "is"   ($#v1_connsp_1 :::"connected"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_connsp_1 :::"connected"::: )  )) ; 
 registrationlet "T" be   ($#v1_connsp_1 :::"connected"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" "T") "#)" ) ->   ($#v1_connsp_1 :::"connected"::: )   ; 
end; 
theorem :: TOPALG_3:9 (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_borsuk_2 :::"pathwise_connected"::: )  )) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_borsuk_2 :::"pathwise_connected"::: )  )) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v7_struct_0 :::"trivial"::: )     ($#v2_pre_topc :::"TopSpace-like"::: )    ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_borsuk_2 :::"pathwise_connected"::: )    for    ($#l1_pre_topc :::"TopStruct"::: )  ; 
end; 
theorem :: TOPALG_3:10 (Bool  "for" (Set (Var "T")) "being"    ($#m1_pre_topc :::"SubSpace"::: )   "of" (Set   ($#k15_euclid :::"TOP-REAL"::: )  (Num 2))  "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "is"   ($#m1_subset_1 :::"Simple_closed_curve":::))) "holds"  (Bool (Set (Var "T")) "is"   ($#v1_borsuk_2 :::"pathwise_connected"::: )  )) ; 
 
theorem :: TOPALG_3:11 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) (Bool  "ex" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "F")) "is"   ($#m1_setfam_1 :::"Cover":::) "of" (Set (Var "T"))) & (Bool (Set (Var "F")) "is"   ($#v1_tops_2 :::"open"::: )  )  ")" ))) ; 
 registrationlet "T" be   ($#l1_pre_topc :::"TopSpace":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_tops_2 :::"open"::: )     ($#v2_tops_2 :::"closed"::: )     ($#v4_taxonom2 :::"mutually-disjoint"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "T") ")" )); 
end; 
theorem :: TOPALG_3:12 (Bool  "for" (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "D")) "being"   ($#v1_tops_2 :::"open"::: )     ($#v4_taxonom2 :::"mutually-disjoint"::: )    ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_connsp_1 :::"connected"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "D"))) & (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"meets"::: )  (Set (Var "A"))) & (Bool (Set (Var "D")) "is"    ($#m1_setfam_1 :::"Cover"::: )   "of" (Set (Var "A")))) "holds"  (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))))))) ; 
 begin  
theorem :: TOPALG_3:13 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::) "holds"  (Bool (Set   ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) )) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) )) "#)" )  ($#r1_hidden :::"="::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "S"))) "#)" ) "," (Set  ($#g1_pre_topc :::"TopStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) "," (Set  "the"  ($#u1_pre_topc :::"topology"::: )  "of" (Set (Var "T"))) "#)" ) ($#k2_borsuk_1 :::":]"::: ) ))) ; 
 
theorem :: TOPALG_3:14 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k2_pre_topc :::"Cl"::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k3_borsuk_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k2_pre_topc :::"Cl"::: )  (Set (Var "B")) ")" ) ($#k3_borsuk_1 :::":]"::: ) ))))) ; 
 
theorem :: TOPALG_3:15 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds"  (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k3_borsuk_1 :::":]"::: ) ) "is"   ($#v4_pre_topc :::"closed"::: )  )))) ; 
 registrationlet "A", "B" be   ($#v1_connsp_1 :::"connected"::: )    ($#l1_pre_topc :::"TopSpace":::); 
cluster (Set  ($#k2_borsuk_1 :::"[:"::: ) "A" "," "B" ($#k2_borsuk_1 :::":]"::: ) ) ->   ($#v1_connsp_1 :::"connected"::: )   ; 
end; 
theorem :: TOPALG_3:16 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v2_connsp_1 :::"connected"::: )  ) & (Bool (Set (Var "B")) "is"   ($#v2_connsp_1 :::"connected"::: )  )) "holds"  (Bool (Set  ($#k3_borsuk_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k3_borsuk_1 :::":]"::: ) ) "is"   ($#v2_connsp_1 :::"connected"::: )  )))) ; 
 
theorem :: TOPALG_3:17 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (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":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set  "(" (Set (Var "S"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "T"))) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))))) ; 
 
theorem :: TOPALG_3:18 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (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":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set  "(" (Set (Var "T"))  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v5_pre_topc :::"continuous"::: )  )))))) ; 
 
theorem :: TOPALG_3:19 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "Y")) "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  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "T1")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "S"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "S"))  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "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 (Var "F1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1")))) & (Bool (Set (Var "F2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")))) & (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 "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  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "T1")) ($#k2_borsuk_1 :::":]"::: ) ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "T2")) ($#k2_borsuk_1 :::":]"::: ) ) ")" )))) "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  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (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"::: )  )  ")" )))))) ; 
 
theorem :: TOPALG_3:20 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "Y")) "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  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "S"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T2")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "S"))  (Bool  "for" (Set (Var "F1")) "," (Set (Var "F2")) "being"   ($#v4_pre_topc :::"closed"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))  "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 (Var "F1"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T1")))) & (Bool (Set (Var "F2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "T2")))) & (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 "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  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T1")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T2")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) ")" )))) "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  ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "T")) "," (Set (Var "Y")) ($#k2_borsuk_1 :::":]"::: ) ) "," (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"::: )  )  ")" )))))) ; 
 begin  registrationlet "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "t" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); 
cluster   ->   ($#v5_pre_topc :::"continuous"::: )    for    ($#m1_borsuk_2 :::"Path"::: )   "of" "t" "," "t"; 
end; 
theorem :: TOPALG_3:21 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  ($#k17_borsuk_1 :::"I[01]"::: ) )  (Bool  "for" (Set (Var "P")) "being"   ($#v3_funct_1 :::"constant"::: )    ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "t")) "holds"  (Bool (Set (Set (Var "P"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "t"))))))) ; 
 
theorem :: TOPALG_3:22 (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "t")) "holds"   (Bool  "("  (Bool (Set (Set (Var "P"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "t"))) & (Bool (Set (Set (Var "P"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "t")))  ")" )))) ; 
 
theorem :: TOPALG_3:23 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_borsuk_6 :::"are_connected"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  ($#r1_borsuk_6 :::"are_connected"::: )  )))) ; 
 
theorem :: TOPALG_3:24 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (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"))  ($#r1_borsuk_6 :::"are_connected"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "P"))) "is"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))))))) ; 
 
theorem :: TOPALG_3:25 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_borsuk_2 :::"pathwise_connected"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T")) "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 "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "P"))) "is"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b"))))))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_borsuk_2 :::"pathwise_connected"::: )    ($#l1_pre_topc :::"TopSpace":::); let "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 "S")); let "P" be    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Const "a")) "," (Set (Const "b")); let "f" be   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); :: original: :::"*"::: redefine func "f" :::"*"::: "P" ->    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set "f"  ($#k3_funct_2 :::"."::: )  "a") "," (Set "f"  ($#k3_funct_2 :::"."::: )  "b"); end; 
theorem :: TOPALG_3:26 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "P"))) "is"   ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))))) ; 
 definitionlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "a" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "P" be   ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Const "a")); let "f" be   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); :: original: :::"*"::: redefine func "f" :::"*"::: "P" ->   ($#m1_borsuk_2 :::"Loop":::) "of" (Set "f"  ($#k3_funct_2 :::"."::: )  "a"); end; 
theorem :: TOPALG_3:27 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "P1")) "," (Set (Var "Q1")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  "st" (Bool (Bool (Set (Var "P")) "," (Set (Var "Q"))  ($#r3_borsuk_2 :::"are_homotopic"::: )  ) & (Bool (Set (Var "P1"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "P")))) & (Bool (Set (Var "Q1"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "Q"))))) "holds"  (Bool (Set (Var "P1")) "," (Set (Var "Q1"))  ($#r3_borsuk_2 :::"are_homotopic"::: )  )))))) ; 
 
theorem :: TOPALG_3:28 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "P")) "," (Set (Var "Q")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "a")) "," (Set (Var "b"))  (Bool  "for" (Set (Var "P1")) "," (Set (Var "Q1")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  (Bool  "for" (Set (Var "F")) "being"    ($#m1_borsuk_6 :::"Homotopy"::: )   "of" (Set (Var "P")) "," (Set (Var "Q"))  "st" (Bool (Bool (Set (Var "P")) "," (Set (Var "Q"))  ($#r3_borsuk_2 :::"are_homotopic"::: )  ) & (Bool (Set (Var "P1"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "P")))) & (Bool (Set (Var "Q1"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "Q"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "F"))) "is"    ($#m1_borsuk_6 :::"Homotopy"::: )   "of" (Set (Var "P1")) "," (Set (Var "Q1"))))))))) ; 
 
theorem :: TOPALG_3:29 (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"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (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"))  (Bool  "for" (Set (Var "P1")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b")))  (Bool  "for" (Set (Var "Q1")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b"))) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "c")))  "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b"))  ($#r1_borsuk_6 :::"are_connected"::: )  ) & (Bool (Set (Var "b")) "," (Set (Var "c"))  ($#r1_borsuk_6 :::"are_connected"::: )  ) & (Bool (Set (Var "P1"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "P")))) & (Bool (Set (Var "Q1"))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "Q"))))) "holds"  (Bool (Set (Set (Var "P1"))  ($#k1_borsuk_2 :::"+"::: )  (Set (Var "Q1")))  ($#r2_funct_2 :::"="::: )  (Set (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set  "(" (Set (Var "P"))  ($#k1_borsuk_2 :::"+"::: )  (Set (Var "Q")) ")" )))))))))) ; 
 definitionlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "s" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); assume 
(Bool (Set (Const "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )
 ; func  :::"FundGrIso":::  "(" "f" "," "s" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" "S" "," "s" ")"  ")" ) "," (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" "T" "," (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  "s" ")" ) ")"  ")" ) means :: TOPALG_3:def 1 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" "S" "," "s" ")"  ")" ) (Bool  "ex" (Set (Var "ls")) "being"   ($#m1_borsuk_2 :::"Loop":::) "of" "s" "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k4_topalg_1 :::"EqRel"::: )   "(" "S" "," "s" ")"  ")" ) "," (Set (Var "ls")) ")" )) & (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k4_topalg_1 :::"EqRel"::: )   "(" "T" "," (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  "s" ")" ) ")"  ")" ) "," (Set  "(" "f"  ($#k1_partfun1 :::"*"::: )  (Set (Var "ls")) ")" ) ")" ))  ")" ))); end; 









:: deftheorem    defines :::"FundGrIso"::: TOPALG_3:def 1 :  (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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v5_pre_topc :::"continuous"::: )  )) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" (Set (Var "S")) "," (Set (Var "s")) ")"  ")" ) "," (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" (Set (Var "T")) "," (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")) ")" ) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_topalg_3 :::"FundGrIso"::: )   "(" (Set (Var "f")) "," (Set (Var "s")) ")" )) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" (Set (Var "S")) "," (Set (Var "s")) ")"  ")" ) (Bool  "ex" (Set (Var "ls")) "being"   ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "s")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k4_topalg_1 :::"EqRel"::: )   "(" (Set (Var "S")) "," (Set (Var "s")) ")"  ")" ) "," (Set (Var "ls")) ")" )) & (Bool (Set (Set (Var "b5"))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k4_topalg_1 :::"EqRel"::: )   "(" (Set (Var "T")) "," (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")) ")" ) ")"  ")" ) "," (Set  "(" (Set (Var "f"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "ls")) ")" ) ")" ))  ")" )))  ")" ))))); 
 
theorem :: TOPALG_3:30 (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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "ls")) "being"   ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "s")) "holds"  (Bool (Set (Set  "("  ($#k3_topalg_3 :::"FundGrIso"::: )   "(" (Set (Var "f")) "," (Set (Var "s")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k4_topalg_1 :::"EqRel"::: )   "(" (Set (Var "S")) "," (Set (Var "s")) ")"  ")" ) "," (Set (Var "ls")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k4_topalg_1 :::"EqRel"::: )   "(" (Set (Var "T")) "," (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")) ")" ) ")"  ")" ) "," (Set  "(" (Set (Var "f"))  ($#k2_topalg_3 :::"*"::: )  (Set (Var "ls")) ")" ) ")" )))))) ; 
 registrationlet "S", "T" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::); let "s" be   ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "f" be   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Const "S")) "," (Set (Const "T")); 
cluster (Set   ($#k3_topalg_3 :::"FundGrIso"::: )   "(" "f" "," "s" ")" ) ->   ($#v1_group_6 :::"multiplicative"::: )   ; 
end; 
theorem :: TOPALG_3:31 (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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#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   ($#k3_topalg_3 :::"FundGrIso"::: )   "(" (Set (Var "f")) "," (Set (Var "s")) ")" ) "is"   ($#v3_funct_2 :::"bijective"::: )  )))) ; 
 
theorem :: TOPALG_3:32 (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 "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "f")) "being"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_borsuk_2 :::"Path"::: )   "of" (Set (Var "t")) "," (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s")))  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" (Set (Var "S")) "," (Set (Var "s")) ")"  ")" ) "," (Set  "("  ($#k5_topalg_1 :::"pi_1"::: )   "(" (Set (Var "T")) "," (Set (Var "t")) ")"  ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v3_tops_2 :::"being_homeomorphism"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "s"))) "," (Set (Var "t"))  ($#r1_borsuk_6 :::"are_connected"::: )  ) & (Bool (Set (Var "h"))  ($#r2_funct_2 :::"="::: )  (Set (Set  "("  ($#k6_topalg_1 :::"pi_1-iso"::: )  (Set (Var "P")) ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "("  ($#k3_topalg_3 :::"FundGrIso"::: )   "(" (Set (Var "f")) "," (Set (Var "s")) ")"  ")" )))) "holds"  (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ))))))) ; 
 
theorem :: TOPALG_3:33 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "T")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_borsuk_2 :::"pathwise_connected"::: )    ($#l1_pre_topc :::"TopSpace":::)  (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T"))  ($#r2_borsuk_3 :::"are_homeomorphic"::: )  )) "holds"  (Bool (Set   ($#k5_topalg_1 :::"pi_1"::: )   "(" (Set (Var "S")) "," (Set (Var "s")) ")" ) "," (Set   ($#k5_topalg_1 :::"pi_1"::: )   "(" (Set (Var "T")) "," (Set (Var "t")) ")" )  ($#r2_group_6 :::"are_isomorphic"::: )  ))))) ;