:: TREAL_1 semantic presentation begin theorem :: TREAL_1:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (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_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v4_pre_topc :::"closed"::: ) ))) ; theorem :: TREAL_1:2 (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 ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_borsuk_1 :::"closed"::: ) )) ; theorem :: TREAL_1:3 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "d")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d")))) "holds" (Bool (Set ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) "is" ($#v1_borsuk_1 :::"closed"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; theorem :: TREAL_1:4 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "d"))) & (Bool (Set (Var "c")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k1_tsep_1 :::"union"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ))) & (Bool (Set ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k2_tsep_1 :::"meet"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ))) ")" )) ; definitionlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "b"))) ; func :::"(#)"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" "a" "," "b" ")" ")" ) equals :: TREAL_1:def 1 "a"; func "(" "a" "," "b" ")" :::"(#)"::: -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" "a" "," "b" ")" ")" ) equals :: TREAL_1:def 2 "b"; end; :: deftheorem defines :::"(#)"::: TREAL_1:def 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")))) "holds" (Bool (Set ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))); :: deftheorem defines :::"(#)"::: TREAL_1:def 2 : (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 (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b")))); theorem :: TREAL_1:5 (Bool "(" (Bool (Set ($#k18_borsuk_1 :::"0[01]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" )) & (Bool (Set ($#k19_borsuk_1 :::"1[01]"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) )) ")" ) ; theorem :: TREAL_1:6 (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")))) "holds" (Bool "(" (Bool (Set ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) & (Bool (Set "(" (Set (Var "b")) "," (Set (Var "c")) ")" ($#k2_treal_1 :::"(#)"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "c")) ")" ($#k2_treal_1 :::"(#)"::: ) )) ")" )) ; begin definitionlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Const "b"))) ; let "t1", "t2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Const "a")) "," (Set (Const "b")) ")" ")" ); func :::"L[01]"::: "(" "t1" "," "t2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" "a" "," "b" ")" ")" ) means :: TREAL_1:def 3 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ($#k8_real_1 :::"*"::: ) "t1" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) "t2" ")" )))); end; :: deftheorem defines :::"L[01]"::: TREAL_1:def 3 : (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_treal_1 :::"L[01]"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "t1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "s")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t2")) ")" )))) ")" )))); theorem :: TREAL_1:7 (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "holds" (Bool (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "t2")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t1"))))))) ; theorem :: TREAL_1:8 (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool (Set ($#k3_treal_1 :::"L[01]"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: TREAL_1:9 (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) & (Bool (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ))) ; theorem :: TREAL_1:10 (Bool (Set ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ))) ; definitionlet "a", "b" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; assume (Bool (Set (Const "a")) ($#r1_xxreal_0 :::"<"::: ) (Set (Const "b"))) ; let "t1", "t2" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ); func :::"P[01]"::: "(" "a" "," "b" "," "t1" "," "t2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" "a" "," "b" ")" ")" ) "," (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) means :: TREAL_1:def 4 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" "a" "," "b" ")" ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" "b" ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) "t1" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) "a" ")" ) ($#k3_xcmplx_0 :::"*"::: ) "t2" ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" "b" ($#k6_xcmplx_0 :::"-"::: ) "a" ")" )))); end; :: deftheorem defines :::"P[01]"::: TREAL_1:def 4 : (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "t1")) "," (Set (Var "t2")) ")" )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t1")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t2")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" )))) ")" )))); theorem :: TREAL_1:11 (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "holds" (Bool (Set (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "t2")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t1")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t1")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "t2")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "b")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ")" )))))) ; theorem :: TREAL_1:12 (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "holds" (Bool (Set ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "t1")) "," (Set (Var "t2")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: TREAL_1:13 (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 "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "t1"))) & (Bool (Set (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "t2"))) ")" ))) ; theorem :: TREAL_1:14 (Bool (Set ($#k4_treal_1 :::"P[01]"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ))) ; theorem :: TREAL_1:15 (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 "(" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#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 :::"(#)"::: ) ")" ) ")" ")" ))) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (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 :::"(#)"::: ) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ")" ))) ")" )) ; theorem :: TREAL_1:16 (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 "(" (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ")" ))) & (Bool (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ")" ))) ")" )) ; theorem :: TREAL_1:17 (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 "(" (Bool (Set ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (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 :::"(#)"::: ) ")" ) ")" )) & (Bool (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 :::"(#)"::: ) ")" ) ")" ) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (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 :::"(#)"::: ) ")" ) ")" ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) ")" )) ")" )) ; theorem :: TREAL_1:18 (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 "(" (Bool (Set ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Set "(" ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" )) & (Bool (Set ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Set "(" ($#k4_treal_1 :::"P[01]"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ")" ) ")" ")" ) ($#k2_tops_2 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_treal_1 :::"L[01]"::: ) "(" (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k2_treal_1 :::"(#)"::: ) ")" ) "," (Set "(" ($#k1_treal_1 :::"(#)"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" )) ")" )) ; begin theorem :: TREAL_1:19 (Bool (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "is" ($#v1_connsp_1 :::"connected"::: ) ) ; theorem :: TREAL_1:20 (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 ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_connsp_1 :::"connected"::: ) )) ; theorem :: TREAL_1:21 (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "st" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: TREAL_1:22 (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 "for" (Set (Var "f")) "being" ($#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 "a")) "," (Set (Var "b")) ")" ")" ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "st" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: TREAL_1:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y")))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) ")" ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: TREAL_1:24 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) ")" ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "st" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ;