:: BORSUK_5 semantic presentation begin theorem :: BORSUK_5:1 canceled; theorem :: BORSUK_5:2 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x3")) "," (Set (Var "x6")) ($#k1_enumset1 :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x2")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: BORSUK_5:3 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#r4_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Num 6))) ; theorem :: BORSUK_5:4 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#r5_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Num 7))) ; theorem :: BORSUK_5:5 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k1_enumset1 :::"}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x5"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x6"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x5"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set (Var "x6"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x4"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x5"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set (Var "x6"))) ")" )) ; theorem :: BORSUK_5:6 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k1_enumset1 :::"}"::: ) ))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#r4_zfmisc_1 :::"are_mutually_different"::: ) )) ; theorem :: BORSUK_5:7 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#r4_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ) ($#r1_subset_1 :::"misses"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x7")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#r5_zfmisc_1 :::"are_mutually_different"::: ) )) ; theorem :: BORSUK_5:8 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#r5_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set (Var "x7")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#r5_zfmisc_1 :::"are_mutually_different"::: ) )) ; theorem :: BORSUK_5:9 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#r5_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x5")) "," (Set (Var "x3")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x4")) ($#r5_zfmisc_1 :::"are_mutually_different"::: ) )) ; registration cluster (Set ($#k3_topmetr :::"R^1"::: ) ) -> ($#v1_borsuk_2 :::"pathwise_connected"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_connsp_1 :::"connected"::: ) for ($#l1_pre_topc :::"TopStruct"::: ) ; end; begin theorem :: BORSUK_5:10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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 "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "d"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ))) ; theorem :: BORSUK_5:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "c")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: BORSUK_5:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "c")) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ))) ; registration cluster -> ($#v1_xreal_0 :::"real"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_numbers :::"RAT"::: ) ); end; theorem :: BORSUK_5:13 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k8_metric_1 :::"RealSpace"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "A")))) ")" ))) ; theorem :: BORSUK_5:14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k8_metric_1 :::"RealSpace"::: ) ) "st" (Bool (Bool (Set (Var "q")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "p"))))) ; theorem :: BORSUK_5:15 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) )))) ; theorem :: BORSUK_5:16 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) ; begin registration cluster (Set ($#k7_power :::"number_e"::: ) ) -> ($#v1_rat_1 :::"irrational"::: ) ; end; definitionfunc :::"IRRAT"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: BORSUK_5:def 1 (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k3_numbers :::"RAT"::: ) )); end; :: deftheorem defines :::"IRRAT"::: BORSUK_5:def 1 : (Bool (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k3_numbers :::"RAT"::: ) ))); definitionlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"RAT"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: BORSUK_5:def 2 (Set (Set ($#k3_numbers :::"RAT"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) "a" "," "b" ($#k2_rcomp_1 :::".["::: ) )); func :::"IRRAT"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: BORSUK_5:def 3 (Set (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) "a" "," "b" ($#k2_rcomp_1 :::".["::: ) )); end; :: deftheorem defines :::"RAT"::: BORSUK_5:def 2 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_numbers :::"RAT"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))); :: deftheorem defines :::"IRRAT"::: BORSUK_5:def 3 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))); theorem :: BORSUK_5:17 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_rat_1 :::"irrational"::: ) ) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_borsuk_5 :::"IRRAT"::: ) )) ")" )) ; registration cluster ($#v1_xcmplx_0 :::"complex"::: ) ($#v1_xreal_0 :::"real"::: ) ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_rat_1 :::"irrational"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; let "b" be ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k2_xcmplx_0 :::"+"::: ) "b") -> ($#v1_rat_1 :::"irrational"::: ) ; cluster (Set "b" ($#k2_xcmplx_0 :::"+"::: ) "a") -> ($#v1_rat_1 :::"irrational"::: ) ; end; theorem :: BORSUK_5:18 (Bool "for" (Set (Var "a")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b"))) "is" ($#v1_rat_1 :::"irrational"::: ) ))) ; registrationlet "a" be ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_xcmplx_0 :::"-"::: ) "a") -> ($#v1_rat_1 :::"irrational"::: ) ; end; theorem :: BORSUK_5:19 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a"))) "is" ($#v1_rat_1 :::"irrational"::: ) )) ; registrationlet "a" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; let "b" be ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k6_xcmplx_0 :::"-"::: ) "b") -> ($#v1_rat_1 :::"irrational"::: ) ; cluster (Set "b" ($#k6_xcmplx_0 :::"-"::: ) "a") -> ($#v1_rat_1 :::"irrational"::: ) ; end; theorem :: BORSUK_5:20 (Bool "for" (Set (Var "a")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b"))) "is" ($#v1_rat_1 :::"irrational"::: ) ))) ; theorem :: BORSUK_5:21 (Bool "for" (Set (Var "a")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a"))) "is" ($#v1_rat_1 :::"irrational"::: ) ))) ; theorem :: BORSUK_5:22 (Bool "for" (Set (Var "a")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b"))) "is" ($#v1_rat_1 :::"irrational"::: ) ))) ; theorem :: BORSUK_5:23 (Bool "for" (Set (Var "a")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "b")) ($#k13_complex1 :::"/"::: ) (Set (Var "a"))) "is" ($#v1_rat_1 :::"irrational"::: ) ))) ; registration cluster ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xreal_0 :::"real"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: BORSUK_5:24 (Bool "for" (Set (Var "a")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k13_complex1 :::"/"::: ) (Set (Var "b"))) "is" ($#v1_rat_1 :::"irrational"::: ) ))) ; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_int_1 :::"frac"::: ) "r") -> ($#v1_rat_1 :::"irrational"::: ) ; end; theorem :: BORSUK_5:25 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_int_1 :::"frac"::: ) (Set (Var "r"))) "is" ($#v1_rat_1 :::"irrational"::: ) )) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xcmplx_0 :::"complex"::: ) ($#v1_xreal_0 :::"real"::: ) ($#v1_xxreal_0 :::"ext-real"::: ) ($#v1_rat_1 :::"rational"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "a" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; let "b" be ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "a" ($#k3_xcmplx_0 :::"*"::: ) "b") -> ($#v1_rat_1 :::"irrational"::: ) ; cluster (Set "b" ($#k3_xcmplx_0 :::"*"::: ) "a") -> ($#v1_rat_1 :::"irrational"::: ) ; cluster (Set "a" ($#k7_xcmplx_0 :::"/"::: ) "b") -> ($#v1_rat_1 :::"irrational"::: ) ; cluster (Set "b" ($#k7_xcmplx_0 :::"/"::: ) "a") -> ($#v1_rat_1 :::"irrational"::: ) ; end; theorem :: BORSUK_5:26 (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 "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p1"))) & (Bool (Set (Var "p1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) ")" ))) ; theorem :: BORSUK_5:27 (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 "ex" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v1_rat_1 :::"irrational"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) ")" ))) ; theorem :: BORSUK_5:28 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) )))) ; theorem :: BORSUK_5:29 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "c")) "is" ($#v1_rat_1 :::"rational"::: ) ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) ")" ) ")" )) ; theorem :: BORSUK_5:30 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set (Var "c")) "is" ($#v1_rat_1 :::"irrational"::: ) ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) ")" ) ")" )) ; theorem :: BORSUK_5:31 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:32 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:33 (Bool "for" (Set (Var "T")) "being" ($#v1_connsp_1 :::"connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#v3_pre_topc :::"open"::: ) ($#v4_pre_topc :::"closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T")))) ")" ))) ; theorem :: BORSUK_5:34 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ) & (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ) & (Bool (Bool "not" (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; begin theorem :: BORSUK_5:35 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:36 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:37 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k4_rcomp_1 :::".]"::: ) ))) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c")))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "c")) ($#k1_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:38 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "a")) ($#k1_seq_4 :::"}"::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "a")) ($#k1_seq_4 :::"}"::: ) )))) ; theorem :: BORSUK_5:39 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_rcomp_1 :::"open"::: ) ) "iff" (Bool (Set (Var "B")) "is" ($#v3_pre_topc :::"open"::: ) ) ")" ))) ; registrationlet "A", "B" be ($#v3_rcomp_1 :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "A" ($#k3_xboole_0 :::"/\"::: ) "B") -> ($#v3_rcomp_1 :::"open"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "A" ($#k2_xboole_0 :::"\/"::: ) "B") -> ($#v3_rcomp_1 :::"open"::: ) for ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: BORSUK_5:40 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; theorem :: BORSUK_5:41 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: BORSUK_5:42 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: BORSUK_5:43 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "a")) ($#k1_seq_4 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )))) ; theorem :: BORSUK_5:44 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "a")) ($#k1_seq_4 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) )))) ; registrationlet "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set bbbadK4_XXREAL_1("a" "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ))) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set bbbadK3_XXREAL_1((Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," "a")) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set bbbadK4_XXREAL_1((Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," "a")) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set bbbadK2_XXREAL_1("a" "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ))) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: BORSUK_5:45 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: BORSUK_5:46 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: BORSUK_5:47 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: BORSUK_5:48 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: BORSUK_5:49 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )))) ; theorem :: BORSUK_5:50 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_measure6 :::"Cl"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: BORSUK_5:51 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:52 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_measure6 :::"Cl"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ))) ; theorem :: BORSUK_5:53 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) ))) ; theorem :: BORSUK_5:54 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )))) ; theorem :: BORSUK_5:55 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )))) ; theorem :: BORSUK_5:56 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set (Var "c")) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "c")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )))) ; theorem :: BORSUK_5:57 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; theorem :: BORSUK_5:58 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k2_borsuk_5 :::"RAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )))) ; theorem :: BORSUK_5:59 (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 (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "a")) ($#k1_seq_4 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "b")) ($#k1_seq_4 :::"}"::: ) )))) ; theorem :: BORSUK_5:60 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_borsuk_5 :::"RAT"::: ) "(" (Num 2) "," (Num 4) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 4) "," (Num 5) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 5) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 2) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Num 2) "," (Num 4) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 4) ($#k1_seq_4 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 5) ($#k1_seq_4 :::"}"::: ) )))) ; theorem :: BORSUK_5:61 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "a")) ($#k1_seq_4 :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))))) ; theorem :: BORSUK_5:62 (Bool (Set (Set "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Num 1) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 2) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Num 2) "," (Num 4) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 4) ($#k1_seq_4 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 5) ($#k1_seq_4 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Num 1) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Num 1) "," (Num 2) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Num 2) "," (Num 4) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 4) ($#k1_seq_4 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Num 5) ($#k1_seq_4 :::"}"::: ) ))) ; theorem :: BORSUK_5:63 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "a")) ($#k1_seq_4 :::"}"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) )))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ))))) ; theorem :: BORSUK_5:64 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:65 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:66 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "c")) ($#k1_seq_4 :::"}"::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "c")) ($#k4_rcomp_1 :::".]"::: ) )))) ; theorem :: BORSUK_5:67 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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 "b")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "c"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_borsuk_5 :::"IRRAT"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "c")) ($#k1_seq_4 :::"}"::: ) ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "d")) ($#k1_seq_4 :::"}"::: ) )))) "holds" (Bool (Set ($#k2_pre_topc :::"Cl"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "c")) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "d")) ($#k1_seq_4 :::"}"::: ) ))))) ; theorem :: BORSUK_5:68 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "b")) ($#k1_seq_4 :::"}"::: ) )))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "b")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))))) ; theorem :: BORSUK_5:69 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "b")) ($#k1_seq_4 :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: BORSUK_5:70 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "a")) ($#k4_rcomp_1 :::".]"::: ) ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set (Var "b")) ($#k1_seq_4 :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: BORSUK_5:71 (Bool "for" (Set (Var "TS")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "TS")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "B")) ($#k3_subset_1 :::"`"::: ) )))) ; theorem :: BORSUK_5:72 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set ($#k1_numbers :::"REAL"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; begin theorem :: BORSUK_5:73 (Bool "for" (Set (Var "X")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "X9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X9")) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Var "X9")) "is" ($#v4_xxreal_2 :::"bounded_above"::: ) ) & (Bool (Set (Var "X9")) "is" ($#v3_xxreal_2 :::"bounded_below"::: ) ) ")" ))) ; theorem :: BORSUK_5:74 (Bool "for" (Set (Var "X")) "being" ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "X9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X9"))) & (Bool (Set (Var "X9")) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "X9"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "X9")))) ")" )))) ; theorem :: BORSUK_5:75 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "C9")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Var "C9"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "C9")) ")" ) "," (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "C9")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "C9")))) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k5_seq_4 :::"lower_bound"::: ) (Set (Var "C9")) ")" ) "," (Set "(" ($#k4_seq_4 :::"upper_bound"::: ) (Set (Var "C9")) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "C9"))))) ; theorem :: BORSUK_5:76 (Bool "for" (Set (Var "A")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))))) ; theorem :: BORSUK_5:77 (Bool "for" (Set (Var "A")) "being" ($#v2_connsp_1 :::"connected"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) ; theorem :: BORSUK_5:78 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool (Set (Var "X")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_measure5 :::"closed_interval"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ))) ; theorem :: BORSUK_5:79 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_connsp_1 :::"connected"::: ) ($#v2_compts_1 :::"compact"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "ex" (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"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) ")" ))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_tops_2 :::"open"::: ) ($#v2_tops_2 :::"closed"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T") ")" )); end;