:: BORSUK_6 semantic presentation begin scheme :: BORSUK_6:sch 1 ExFunc3CondD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) ], P3[ ($#m1_hidden :::"set"::: ) ], F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "c")) ")" )) ")" & "(" (Bool (Bool P3[(Set (Var "c"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P2[(Set (Var "c"))])) ")" & "(" (Bool (Bool P1[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" & "(" (Bool (Bool P2[(Set (Var "c"))])) "implies" (Bool "not" (Bool P3[(Set (Var "c"))])) ")" ")" )) and (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool P1[(Set (Var "c"))]) "or" (Bool P2[(Set (Var "c"))]) "or" (Bool P3[(Set (Var "c"))]) ")" )) proof end; theorem :: BORSUK_6:1 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) )) ; theorem :: BORSUK_6:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" )) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" )))) ; theorem :: BORSUK_6:3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) ; theorem :: BORSUK_6:4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1)) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) ; theorem :: BORSUK_6:5 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "q"))) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) ; theorem :: BORSUK_6:6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x"))) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) ; theorem :: BORSUK_6:7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set (Set (Var "x")) ($#k5_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ))) ; theorem :: BORSUK_6:8 (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) )) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k18_borsuk_1 :::"0[01]"::: ) ) "," (Set ($#k19_borsuk_1 :::"1[01]"::: ) )) ; theorem :: BORSUK_6:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ))) ; begin theorem :: BORSUK_6:10 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" ) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) )) "}" )) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "T")))) ; theorem :: BORSUK_6:11 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" ) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) )) "}" )) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "T")))) ; theorem :: BORSUK_6:12 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) "}" ) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ))) "}" )) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "T")))) ; theorem :: BORSUK_6:13 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) "}" ) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ))) "}" )) "holds" (Bool (Set (Set "(" ($#k2_jgraph_2 :::"AffineMap"::: ) "(" (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k7_relset_1 :::".:"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Var "T")))) ; begin theorem :: BORSUK_6:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v3_topmetr :::"real-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "T")) "holds" (Bool (Set (Var "x")) "is" ($#v1_xreal_0 :::"real"::: ) )) ")" )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_topmetr :::"real-membered"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_topmetr :::"real-membered"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; registrationlet "T" be ($#v3_topmetr :::"real-membered"::: ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster -> ($#v1_xreal_0 :::"real"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T"); end; registrationlet "T" be ($#v3_topmetr :::"real-membered"::: ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster -> ($#v3_topmetr :::"real-membered"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" "T"; end; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_topmetr :::"real-membered"::: ) ($#l1_pre_topc :::"TopSpace":::); let "p" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "T")) ($#k2_borsuk_1 :::":]"::: ) ); cluster (Set "p" ($#k1_xtuple_0 :::"`1"::: ) ) -> ($#v1_xreal_0 :::"real"::: ) ; cluster (Set "p" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_xreal_0 :::"real"::: ) ; end; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set "x" ($#k1_xtuple_0 :::"`1"::: ) ) -> ($#v1_xreal_0 :::"real"::: ) ; cluster (Set "x" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_xreal_0 :::"real"::: ) ; end; begin theorem :: BORSUK_6:15 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ; theorem :: BORSUK_6:16 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ; theorem :: BORSUK_6:17 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ; theorem :: BORSUK_6:18 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ; theorem :: BORSUK_6:19 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ; theorem :: BORSUK_6:20 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )))) ; theorem :: BORSUK_6:21 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ))) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )) ; theorem :: BORSUK_6:22 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )) ; theorem :: BORSUK_6:23 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ))) & (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ) "}" "is" ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )) ; theorem :: BORSUK_6:24 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ))) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )) ; theorem :: BORSUK_6:25 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ))) & (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )) ; theorem :: BORSUK_6:26 (Bool "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )) ; theorem :: BORSUK_6: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 "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S"))) & (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T"))) ")" ))) ; theorem :: BORSUK_6:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) )))) ; theorem :: BORSUK_6:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) ))) "holds" (Bool (Set (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) ($#k1_pre_topc :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k2_struct_0 :::"[#]"::: ) (Set "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; begin registrationlet "T" be ($#l1_pre_topc :::"TopStruct"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v2_compts_1 :::"compact"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; theorem :: BORSUK_6:30 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#v1_xboole_0 :::"empty"::: ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")))) ; theorem :: BORSUK_6:31 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) "is" ($#v1_xboole_0 :::"empty"::: ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T"))))) ; theorem :: BORSUK_6:32 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "is" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ))) ; begin definitionlet "a", "b", "c", "d" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"L[01]"::: "(" "a" "," "b" "," "c" "," "d" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" "a" "," "b" ")" ")" ) "," (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" "c" "," "d" ")" ")" ) equals :: BORSUK_6:def 1 (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" "c" "," "d" ")" ")" ) "," (Set "(" "(" "c" "," "d" ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" "a" "," "b" "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ")" )); end; :: deftheorem defines :::"L[01]"::: BORSUK_6:def 1 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_borsuk_6 :::"L[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) "," (Set "(" "(" (Set (Var "c")) "," (Set (Var "d")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ")" )))); theorem :: BORSUK_6:33 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d")))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_borsuk_6 :::"L[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set "(" ($#k1_borsuk_6 :::"L[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" )) ; theorem :: BORSUK_6:34 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k1_borsuk_6 :::"L[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ))) ; theorem :: BORSUK_6:35 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k1_borsuk_6 :::"L[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")))))) ; theorem :: BORSUK_6:36 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "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 ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) )) ")" )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "r1"))) & (Bool (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "r2"))))) ")" ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))) ; theorem :: BORSUK_6:37 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "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 ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) )) ")" )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "r1"))) & (Bool (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "r2"))))) ")" ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))) ; theorem :: BORSUK_6:38 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "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 ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) )) ")" )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "r1"))) & (Bool (Set (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r2"))))) ")" ) & (Bool (Set (Var "g")) "is" ($#v5_pre_topc :::"continuous"::: ) ) ")" ))) ; begin theorem :: BORSUK_6:39 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ")" )) "is" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")))))) ; theorem :: BORSUK_6:40 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "(" (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )))) ; theorem :: BORSUK_6:41 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "P")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P"))) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); :: original: :::"are_connected"::: redefine pred "a" "," "b" :::"are_connected"::: ; reflexivity (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")) "holds" (Bool bbbadR1_BORSUK_2((Set (Const "T")) "," (Set (Var "b1")) "," (Set (Var "b1"))))) ; symmetry (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")) "st" (Bool (Bool bbbadR1_BORSUK_2((Set (Const "T")) "," (Set (Var "b1")) "," (Set (Var "b2"))))) "holds" (Bool bbbadR1_BORSUK_2((Set (Const "T")) "," (Set (Var "b2")) "," (Set (Var "b1"))))) ; end; theorem :: BORSUK_6:42 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "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 (Set (Var "a")) "," (Set (Var "c")) ($#r1_borsuk_6 :::"are_connected"::: ) ))) ; theorem :: BORSUK_6:43 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "A")) ($#r2_funct_2 :::"="::: ) (Set ($#k2_borsuk_2 :::"-"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "A")) ")" )))))) ; theorem :: BORSUK_6: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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "A")) ($#r2_funct_2 :::"="::: ) (Set ($#k2_borsuk_2 :::"-"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "A")) ")" )))))) ; begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::); let "a", "b", "c" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); let "Q" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "b")) "," (Set (Const "c")); redefine func "P" :::"+"::: "Q" means :: BORSUK_6:def 2 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")) ")" ))) ")" & "(" (Bool (Bool (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t")))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set "Q" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ))) ")" ")" )); end; :: deftheorem defines :::"+"::: BORSUK_6:def 2 : (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 "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "b7")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")) ")" ))) ")" & "(" (Bool (Bool (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "t")))) "implies" (Bool (Set (Set (Var "b7")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ))) ")" ")" )) ")" )))))); definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); redefine func :::"-"::: "P" means :: BORSUK_6:def 3 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set "P" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" )))); end; :: deftheorem defines :::"-"::: BORSUK_6:def 3 : (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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "b5")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" )))) ")" ))))); begin definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ); assume that (Bool (Set (Set (Const "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) and (Bool (Set (Set (Const "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) and (Bool (Set (Const "a")) "," (Set (Const "b")) ($#r1_borsuk_6 :::"are_connected"::: ) ) ; func :::"RePar"::: "(" "P" "," "f" ")" -> ($#m1_borsuk_2 :::"Path"::: ) "of" "a" "," "b" equals :: BORSUK_6:def 4 (Set "P" ($#k1_partfun1 :::"*"::: ) "f"); end; :: deftheorem defines :::"RePar"::: BORSUK_6:def 4 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_borsuk_6 :::"RePar"::: ) "(" (Set (Var "P")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))))))); theorem :: BORSUK_6:45 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_borsuk_6 :::"RePar"::: ) "(" (Set (Var "P")) "," (Set (Var "f")) ")" ) "," (Set (Var "P")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:46 (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 "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k2_borsuk_6 :::"RePar"::: ) "(" (Set (Var "P")) "," (Set (Var "f")) ")" ) "," (Set (Var "P")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; definitionfunc :::"1RP"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) means :: BORSUK_6:def 5 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")))) ")" & "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )); end; :: deftheorem defines :::"1RP"::: BORSUK_6:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_borsuk_6 :::"1RP"::: ) )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")))) ")" & "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )) ")" )); registration cluster (Set ($#k3_borsuk_6 :::"1RP"::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: BORSUK_6:47 (Bool "(" (Bool (Set (Set ($#k3_borsuk_6 :::"1RP"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k3_borsuk_6 :::"1RP"::: ) ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; definitionfunc :::"2RP"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) means :: BORSUK_6:def 6 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ")" )); end; :: deftheorem defines :::"2RP"::: BORSUK_6:def 6 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_borsuk_6 :::"2RP"::: ) )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "t")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ")" )) ")" )); registration cluster (Set ($#k4_borsuk_6 :::"2RP"::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: BORSUK_6:48 (Bool "(" (Bool (Set (Set ($#k4_borsuk_6 :::"2RP"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k4_borsuk_6 :::"2RP"::: ) ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; definitionfunc :::"3RP"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) means :: BORSUK_6:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4)))) "implies" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ")" )); end; :: deftheorem defines :::"3RP"::: BORSUK_6:def 7 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k5_borsuk_6 :::"3RP"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4)))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4)))) "implies" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ")" )) ")" )); registration cluster (Set ($#k5_borsuk_6 :::"3RP"::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: BORSUK_6:49 (Bool "(" (Bool (Set (Set ($#k5_borsuk_6 :::"3RP"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k5_borsuk_6 :::"3RP"::: ) ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; theorem :: BORSUK_6:50 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_borsuk_6 :::"RePar"::: ) "(" (Set (Var "P")) "," (Set ($#k3_borsuk_6 :::"1RP"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")))))))) ; theorem :: BORSUK_6:51 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k2_borsuk_6 :::"RePar"::: ) "(" (Set (Var "P")) "," (Set ($#k4_borsuk_6 :::"2RP"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "Q")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "P")))))))) ; theorem :: BORSUK_6:52 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "R")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "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"::: ) )) "holds" (Bool (Set ($#k2_borsuk_6 :::"RePar"::: ) "(" (Set "(" (Set "(" (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "R")) ")" ) "," (Set ($#k5_borsuk_6 :::"3RP"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "Q")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "R")) ")" )))))))) ; begin definitionfunc :::"LowerLeftUnitTriangle"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) means :: BORSUK_6:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_borsuk_1 :::"]"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ))) ")" )) ")" )); end; :: deftheorem defines :::"LowerLeftUnitTriangle"::: BORSUK_6:def 8 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_borsuk_6 :::"LowerLeftUnitTriangle"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_borsuk_1 :::"]"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ))) ")" )) ")" )) ")" )); notationsynonym :::"IAA"::: for :::"LowerLeftUnitTriangle"::: ; end; definitionfunc :::"UpperUnitTriangle"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) means :: BORSUK_6:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_borsuk_1 :::"]"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" )) ")" )); end; :: deftheorem defines :::"UpperUnitTriangle"::: BORSUK_6:def 9 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k7_borsuk_6 :::"UpperUnitTriangle"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_borsuk_1 :::"]"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" )) ")" )) ")" )); notationsynonym :::"IBB"::: for :::"UpperUnitTriangle"::: ; end; definitionfunc :::"LowerRightUnitTriangle"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) means :: BORSUK_6:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_borsuk_1 :::"]"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" )) ")" )); end; :: deftheorem defines :::"LowerRightUnitTriangle"::: BORSUK_6:def 10 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k8_borsuk_6 :::"LowerRightUnitTriangle"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_borsuk_1 :::"]"::: ) )) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" )) ")" )) ")" )); notationsynonym :::"ICC"::: for :::"LowerRightUnitTriangle"::: ; end; theorem :: BORSUK_6:53 (Bool (Set ($#k6_borsuk_6 :::"IAA"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ))) "}" ) ; theorem :: BORSUK_6:54 (Bool (Set ($#k7_borsuk_6 :::"IBB"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool "(" (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ))) & (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) ")" ) "}" ) ; theorem :: BORSUK_6:55 (Bool (Set ($#k8_borsuk_6 :::"ICC"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" ) ; registration cluster (Set ($#k6_borsuk_6 :::"LowerLeftUnitTriangle"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ; cluster (Set ($#k7_borsuk_6 :::"UpperUnitTriangle"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ; cluster (Set ($#k8_borsuk_6 :::"LowerRightUnitTriangle"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_pre_topc :::"closed"::: ) ; end; theorem :: BORSUK_6:56 (Bool (Set (Set "(" (Set ($#k6_borsuk_6 :::"IAA"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_rcomp_1 :::".]"::: ) ) ($#k8_mcart_1 :::":]"::: ) )) ; theorem :: BORSUK_6:57 (Bool (Set (Set ($#k6_borsuk_6 :::"IAA"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) )) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ))) "}" ) ; theorem :: BORSUK_6:58 (Bool (Set (Set ($#k8_borsuk_6 :::"ICC"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) )) ($#r1_hidden :::"="::: ) "{" (Set (Var "p")) where p "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) : (Bool (Set (Set (Var "p")) ($#k2_xtuple_0 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) "}" ) ; theorem :: BORSUK_6:59 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_borsuk_6 :::"IAA"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: BORSUK_6:60 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: BORSUK_6:61 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_borsuk_6 :::"IAA"::: ) ))) ; theorem :: BORSUK_6:62 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) ))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: BORSUK_6:63 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) ))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: BORSUK_6:64 (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) )) ; theorem :: BORSUK_6:65 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) ))) ; theorem :: BORSUK_6:66 (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) )) ")" ) ; theorem :: BORSUK_6:67 (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) )) ; theorem :: BORSUK_6:68 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Num 1) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) ))) ; theorem :: BORSUK_6:69 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) ))) ; theorem :: BORSUK_6:70 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k6_borsuk_6 :::"IAA"::: ) ))) ; theorem :: BORSUK_6:71 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k7_borsuk_6 :::"IBB"::: ) ))) & (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) ))) ")" )) ; theorem :: BORSUK_6:72 (Bool (Set (Set ($#k6_borsuk_6 :::"IAA"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k8_borsuk_6 :::"ICC"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ; begin theorem :: BORSUK_6:73 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "R")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "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"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "R"))) "," (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "Q")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "R")) ")" )) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: BORSUK_6:74 (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) (Bool "for" (Set (Var "R")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "c1")) "," (Set (Var "d1")) "holds" (Bool (Set (Set "(" (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "R"))) "," (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" (Set (Var "Q")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "R")) ")" )) ($#r4_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: BORSUK_6:75 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q1")) "," (Set (Var "Q2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (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")) "," (Set (Var "P2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) & (Bool (Set (Var "Q1")) "," (Set (Var "Q2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Set (Var "P1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q1"))) "," (Set (Set (Var "P2")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q2"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:76 (Bool "for" (Set (Var "X")) "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 "X")) (Bool "for" (Set (Var "P1")) "," (Set (Var "P2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "Q1")) "," (Set (Var "Q2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "c1")) "st" (Bool (Bool (Set (Var "P1")) "," (Set (Var "P2")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ) & (Bool (Set (Var "Q1")) "," (Set (Var "Q2")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Set (Var "P1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q1"))) "," (Set (Set (Var "P2")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q2"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:77 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "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"::: ) ) & (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P"))) "," (Set ($#k2_borsuk_2 :::"-"::: ) (Set (Var "Q"))) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))) ; theorem :: BORSUK_6:78 (Bool "for" (Set (Var "X")) "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")) "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 "a1")) "," (Set (Var "b1")) "st" (Bool (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P"))) "," (Set ($#k2_borsuk_2 :::"-"::: ) (Set (Var "Q"))) ($#r4_borsuk_2 :::"are_homotopic"::: ) )))) ; theorem :: BORSUK_6:79 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "," (Set (Var "R")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) & (Bool (Set (Var "Q")) "," (Set (Var "R")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "P")) "," (Set (Var "R")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))) ; theorem :: BORSUK_6:80 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q"))) "," (Set (Var "P")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:81 (Bool "for" (Set (Var "X")) "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")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "b1")) "holds" (Bool (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "Q"))) "," (Set (Var "P")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:82 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Set (Var "Q")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "P"))) "," (Set (Var "P")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:83 (Bool "for" (Set (Var "X")) "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")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "a1")) "holds" (Bool (Set (Set (Var "Q")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "P"))) "," (Set (Var "P")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:84 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" )) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:85 (Bool "for" (Set (Var "X")) "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")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "b1")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "a1")) "holds" (Bool (Set (Set (Var "P")) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" )) "," (Set (Var "Q")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:86 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "st" (Bool (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "P"))) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:87 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "b1")) "," (Set (Var "a1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "P")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "b1")) "," (Set (Var "a1")) (Bool "for" (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a1")) "," (Set (Var "a1")) "holds" (Bool (Set (Set "(" ($#k2_borsuk_2 :::"-"::: ) (Set (Var "P")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "P"))) "," (Set (Var "Q")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; theorem :: BORSUK_6:88 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#v3_funct_1 :::"constant"::: ) ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "holds" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P", "Q" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); assume (Bool (Set (Const "P")) "," (Set (Const "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) ; mode :::"Homotopy"::: "of" "P" "," "Q" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," "T" means :: BORSUK_6:def 11 (Bool "(" (Bool it "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set "P" ($#k3_funct_2 :::"."::: ) (Set (Var "t")))) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set "Q" ($#k3_funct_2 :::"."::: ) (Set (Var "t")))) & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) "a") & (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Num 1) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) "b") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Homotopy"::: BORSUK_6:def 11 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "P")) "," (Set (Var "Q"))) "iff" (Bool "(" (Bool (Set (Var "b6")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "b6")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))) & (Bool (Set (Set (Var "b6")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "t")) "," (Num 1) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k3_funct_2 :::"."::: ) (Set (Var "t")))) & (Bool (Set (Set (Var "b6")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set (Var "b6")) ($#k1_binop_1 :::"."::: ) "(" (Num 1) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" ) ")" ) ")" )))));