:: TOPALG_1 semantic presentation begin theorem :: TOPALG_1:1 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "H")) "," (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "H"))))) "holds" (Bool (Set (Var "h")) "is" ($#v3_funct_2 :::"bijective"::: ) )))) ; theorem :: TOPALG_1:2 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k1_rcomp_1 :::".]"::: ) )))) ; theorem :: TOPALG_1:3 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k3_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Set (Var "X")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) )))) ; theorem :: TOPALG_1:4 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Num 1) ($#k4_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPALG_1:5 (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "a")) ($#k3_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Var "X")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: TOPALG_1:6 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "x")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" ($#k6_rvsum_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" ))))) ; theorem :: TOPALG_1:7 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set (Var "x")) ($#k10_rvsum_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "g")) ")" ))))) ; theorem :: TOPALG_1:8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k10_rvsum_1 :::"*"::: ) (Set (Var "f")) ")" ))))) ; theorem :: TOPALG_1:9 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "k")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "g")) ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k4_rvsum_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k4_rvsum_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "k")) ")" )))) ; theorem :: TOPALG_1:10 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "x")) ($#k9_euclid :::"*"::: ) (Set (Var "f")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: TOPALG_1:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k9_euclid :::"*"::: ) (Set (Var "f")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "f")) ($#k12_euclid :::".|"::: ) ))))) ; theorem :: TOPALG_1:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "e3")) "," (Set (Var "e4")) "," (Set (Var "e5")) "," (Set (Var "e6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "e2")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "e3")) ($#r1_hidden :::"="::: ) (Set (Var "p3"))) & (Bool (Set (Var "e4")) ($#r1_hidden :::"="::: ) (Set (Var "p4"))) & (Bool (Set (Var "e5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p3")))) & (Bool (Set (Var "e6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p4")))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e3")) "," (Set (Var "e4")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e5")) "," (Set (Var "e6")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")))))))) ; theorem :: TOPALG_1:13 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "e5")) "," (Set (Var "e6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "e2")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "e5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")))) & (Bool (Set (Var "e6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e5")) "," (Set (Var "e6")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "y")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))))))) ; theorem :: TOPALG_1:14 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "e3")) "," (Set (Var "e4")) "," (Set (Var "e5")) "," (Set (Var "e6")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "p3")) "," (Set (Var "p4")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "e2")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))) & (Bool (Set (Var "e3")) ($#r1_hidden :::"="::: ) (Set (Var "p3"))) & (Bool (Set (Var "e4")) ($#r1_hidden :::"="::: ) (Set (Var "p4"))) & (Bool (Set (Var "e5")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p3")) ")" ))) & (Bool (Set (Var "e6")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "p4")) ")" ))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e1")) "," (Set (Var "e2")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e3")) "," (Set (Var "e4")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "q"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e5")) "," (Set (Var "e6")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "y")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "q")) ")" ))))))) ; theorem :: TOPALG_1:15 (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ))) ")" )) "holds" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ))))) ; theorem :: TOPALG_1:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ))))) ; theorem :: TOPALG_1:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: TOPALG_1:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; begin theorem :: TOPALG_1:19 (Bool "for" (Set (Var "X")) "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 "X")) "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"::: ) )) "holds" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set (Var "A2")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" )) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:20 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set (Var "A2")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" )) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:21 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set (Var "A2")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:22 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "b1")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set (Var "A2")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:23 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "c")) "," (Set (Var "a")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "a")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "A2"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:24 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "a1")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "A2"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:25 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "A2"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:26 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "c1")) "st" (Bool (Bool (Set (Var "A1")) "," (Set (Var "A2")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A1")) "," (Set (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "A2"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:27 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "c")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) "," (Set (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:28 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) "," (Set (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:29 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "a")) "st" (Bool (Bool (Set (Set (Var "C")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "A"))) "," (Set (Set (Var "C")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:30 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "a1")) "st" (Bool (Bool (Set (Set (Var "C")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "A"))) "," (Set (Set (Var "C")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: TOPALG_1:31 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "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 "c")) "," (Set (Var "d")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "d")) "," (Set (Var "e")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d")) "," (Set (Var "e")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))))) ; theorem :: TOPALG_1:32 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "e1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "d1")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d1")) "," (Set (Var "e1")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))))) ; theorem :: TOPALG_1:33 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "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 "c")) "," (Set (Var "d")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "d")) "," (Set (Var "e")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d")) "," (Set (Var "e")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D")) ")" )) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))))) ; theorem :: TOPALG_1:34 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "e1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "d1")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d1")) "," (Set (Var "e1")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D")) ")" )) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))))) ; theorem :: TOPALG_1:35 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "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 "c")) "," (Set (Var "d")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "d")) "," (Set (Var "e")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d")) "," (Set (Var "e")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "C")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D")) ")" )) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))))) ; theorem :: TOPALG_1:36 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "e1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "d1")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d1")) "," (Set (Var "e1")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "C")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D")) ")" )) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))))) ; theorem :: TOPALG_1:37 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "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 "b")) "," (Set (Var "d")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d")) "," (Set (Var "b")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) "," (Set (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_1:38 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "d1")) "," (Set (Var "c1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) "," (Set (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_1:39 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" )) "," (Set (Var "C")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_1:40 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "d1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "c1")) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" )) "," (Set (Var "C")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_1:41 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "d")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "A")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" )) "," (Set (Var "C")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_1:42 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "d1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "c1")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "A")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "B")) ")" )) "," (Set (Var "C")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_1:43 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "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 "c")) "," (Set (Var "d")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "d")) "," (Set (Var "e")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "f")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d")) "," (Set (Var "e")) (Bool "for" (Set (Var "E")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "f")) "," (Set (Var "c")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "E")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "E")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D")) ")" )) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))))))) ; theorem :: TOPALG_1:44 (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 "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "," (Set (Var "d1")) "," (Set (Var "e1")) "," (Set (Var "f1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "B")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "d1")) (Bool "for" (Set (Var "D")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "d1")) "," (Set (Var "e1")) (Bool "for" (Set (Var "E")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "f1")) "," (Set (Var "c1")) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D"))) "," (Set (Set "(" (Set "(" (Set (Var "A")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "B")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "E")) ")" ) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "E")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "C")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "D")) ")" )) ($#r4_borsuk_2 :::"are_homotopic"::: ) )))))))) ; begin definitionlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); mode Loop of "t" is ($#m1_borsuk_2 :::"Path"::: ) "of" "t" "," "t"; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "t1", "t2" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); func :::"Paths"::: "(" "t1" "," "t2" ")" -> ($#m1_hidden :::"set"::: ) means :: TOPALG_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" "t1" "," "t2") ")" )); end; :: deftheorem defines :::"Paths"::: TOPALG_1:def 1 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_topalg_1 :::"Paths"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2"))) ")" )) ")" )))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "t1", "t2" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set ($#k1_topalg_1 :::"Paths"::: ) "(" "t1" "," "t2" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); func :::"Loops"::: "t" -> ($#m1_hidden :::"set"::: ) equals :: TOPALG_1:def 2 (Set ($#k1_topalg_1 :::"Paths"::: ) "(" "t" "," "t" ")" ); end; :: deftheorem defines :::"Loops"::: TOPALG_1:def 2 : (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")) "holds" (Bool (Set ($#k2_topalg_1 :::"Loops"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k1_topalg_1 :::"Paths"::: ) "(" (Set (Var "t")) "," (Set (Var "t")) ")" )))); registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) ; let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set ($#k2_topalg_1 :::"Loops"::: ) "t") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); assume (Bool (Set (Const "a")) "," (Set (Const "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) ; func :::"EqRel"::: "(" "X" "," "a" "," "b" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k1_topalg_1 :::"Paths"::: ) "(" "a" "," "b" ")" ")" ) means :: TOPALG_1:def 3 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" "a" "," "b" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) ")" )); end; :: deftheorem defines :::"EqRel"::: TOPALG_1:def 3 : (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k1_topalg_1 :::"Paths"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "P")) "," (Set (Var "Q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) ")" )) ")" )))); theorem :: TOPALG_1:45 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (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 "Q")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "P")) ")" )) "iff" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) ")" )))) ; theorem :: TOPALG_1:46 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "P")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "Q")) ")" )) "iff" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) ")" )))) ; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"EqRel"::: "(" "X" "," "a" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k2_topalg_1 :::"Loops"::: ) "a" ")" ) equals :: TOPALG_1:def 4 (Set ($#k3_topalg_1 :::"EqRel"::: ) "(" "X" "," "a" "," "a" ")" ); end; :: deftheorem defines :::"EqRel"::: TOPALG_1:def 4 : (Bool "for" (Set (Var "X")) "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 "X")) "holds" (Bool (Set ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "a")) ")" )))); registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set ($#k4_topalg_1 :::"EqRel"::: ) "(" "X" "," "a" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); func :::"FundamentalGroup"::: "(" "X" "," "a" ")" -> ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) means :: TOPALG_1:def 5 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "X" "," "a" ")" ")" ))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" it (Bool "ex" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" "a" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "X" "," "a" ")" ")" ) "," (Set (Var "P")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "X" "," "a" ")" ")" ) "," (Set (Var "Q")) ")" )) & (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "X" "," "a" ")" ")" ) "," (Set "(" (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ")" )) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"FundamentalGroup"::: TOPALG_1:def 5 : (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "b3")) "being" ($#v15_algstr_0 :::"strict"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b3")) (Bool "ex" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "P")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "Q")) ")" )) & (Bool (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b3"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) "," (Set "(" (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ")" )) ")" )) ")" ) ")" ) ")" )))); notationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); synonym :::"pi_1"::: "(" "X" "," "a" ")" for :::"FundamentalGroup"::: "(" "X" "," "a" ")" ; end; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" "X" "," "a" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v15_algstr_0 :::"strict"::: ) ; end; theorem :: TOPALG_1:47 (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ))) "iff" (Bool "ex" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "P")) ")" ))) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "X")); cluster (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" "X" "," "a" ")" ) -> ($#v15_algstr_0 :::"strict"::: ) ($#v2_group_1 :::"Group-like"::: ) ($#v3_group_1 :::"associative"::: ) ; end; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "x0", "x1" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "x0")) "," (Set (Const "x1")); assume (Bool (Set (Const "x0")) "," (Set (Const "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) ) ; func :::"pi_1-iso"::: "P" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" "T" "," "x1" ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" "T" "," "x0" ")" ")" ) means :: TOPALG_1:def 6 (Bool "for" (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" "x1" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "T" "," "x1" ")" ")" ) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "T" "," "x0" ")" ")" ) "," (Set "(" (Set "(" "P" ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) "P" ")" ) ")" ) ")" ))); end; :: deftheorem defines :::"pi_1-iso"::: TOPALG_1:def 6 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "x1")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "x1")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "x0")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "x1")) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "T")) "," (Set (Var "x1")) ")" ")" ) "," (Set (Var "Q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "T")) "," (Set (Var "x0")) ")" ")" ) "," (Set "(" (Set "(" (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" ) ")" ) ")" ))) ")" ))))); theorem :: TOPALG_1:48 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "x1")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "P"))) ($#r2_funct_2 :::"="::: ) (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "Q"))))))) ; theorem :: TOPALG_1:49 (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 "y0")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "R")) "," (Set (Var "V")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "y0")) "," (Set (Var "y1")) "st" (Bool (Bool (Set (Var "R")) "," (Set (Var "V")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "R"))) ($#r2_funct_2 :::"="::: ) (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "V"))))))) ; theorem :: TOPALG_1:50 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "x1")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "P"))) "is" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "x1")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::); let "x0", "x1" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "x0")) "," (Set (Const "x1")); cluster (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) "P") -> ($#v1_group_6 :::"multiplicative"::: ) ; end; theorem :: TOPALG_1:51 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "x1")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "P"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: TOPALG_1:52 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "x1")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "P"))) "is" ($#v2_funct_2 :::"onto"::: ) )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::); let "x0", "x1" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "x0")) "," (Set (Const "x1")); cluster (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) "P") -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ; end; theorem :: TOPALG_1:53 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "x1")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Set "(" ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "P")) ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" )))))) ; theorem :: TOPALG_1:54 (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 "y0")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "R")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "y0")) "," (Set (Var "y1")) "holds" (Bool (Set (Set "(" ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "R")) ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "R")) ")" )))))) ; theorem :: TOPALG_1:55 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "x1")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "x1")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ")" ) "st" (Bool (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "P"))))) "holds" (Bool (Set (Var "h")) "is" ($#v3_funct_2 :::"bijective"::: ) ))))) ; theorem :: TOPALG_1:56 (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 "y0")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "R")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "y0")) "," (Set (Var "y1")) "holds" (Bool (Set ($#k6_topalg_1 :::"pi_1-iso"::: ) (Set (Var "R"))) "is" ($#v3_funct_2 :::"bijective"::: ) )))) ; theorem :: TOPALG_1:57 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x0")) "," (Set (Var "x1")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "x0")) ")" ) "," (Set ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "x1")) ")" ) ($#r2_group_6 :::"are_isomorphic"::: ) ))) ; theorem :: TOPALG_1:58 (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 "y0")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "y0")) ")" ) "," (Set ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "y1")) ")" ) ($#r2_group_6 :::"are_isomorphic"::: ) ))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "P", "Q" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"RealHomotopy"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) means :: TOPALG_1:def 7 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "P" ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "Q" ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )))); end; :: deftheorem defines :::"RealHomotopy"::: TOPALG_1:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_topalg_1 :::"RealHomotopy"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) "iff" (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )))) ")" )))); theorem :: TOPALG_1:59 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "P", "Q" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); cluster -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_borsuk_6 :::"Homotopy"::: ) "of" "P" "," "Q"; end; theorem :: TOPALG_1:60 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "C")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "," "a" ")" ) -> ($#v7_struct_0 :::"trivial"::: ) ($#v15_algstr_0 :::"strict"::: ) ; end; theorem :: TOPALG_1:61 (Bool "for" (Set (Var "S")) "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 "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "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 "P")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "Q")) ")" ))) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) "," (Set "(" (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ")" )))))) ; theorem :: TOPALG_1:62 (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "C")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "holds" (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "C")) ")" ))))) ; theorem :: TOPALG_1:63 (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "P")) ")" )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) ")" ")" ) "," (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" ) ")" ))) "holds" (Bool (Set (Set (Var "x")) ($#k2_group_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "P", "Q" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k7_topalg_1 :::"RealHomotopy"::: ) "(" "P" "," "Q" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPALG_1:64 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set ($#k7_topalg_1 :::"RealHomotopy"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) "is" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "P")) "," (Set (Var "Q")))))) ; theorem :: TOPALG_1:65 (Bool "for" (Set (Var "X")) "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 "X")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v3_relat_2 :::"symmetric"::: ) ) & (Bool (Set ($#k3_topalg_1 :::"EqRel"::: ) "(" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v8_relat_2 :::"transitive"::: ) ) ")" ))) ;