:: BORSUK_5 semantic presentation begin theorem :: BORSUK_5:1 canceled; theorem :: BORSUK_5:2 for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5} proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: {x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5} thus {x1,x2,x3,x4,x5,x6} c= {x1,x3,x6} \/ {x2,x4,x5} :: according to XBOOLE_0:def_10 ::_thesis: {x1,x3,x6} \/ {x2,x4,x5} c= {x1,x2,x3,x4,x5,x6} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x2,x3,x4,x5,x6} or x in {x1,x3,x6} \/ {x2,x4,x5} ) assume x in {x1,x2,x3,x4,x5,x6} ; ::_thesis: x in {x1,x3,x6} \/ {x2,x4,x5} then ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) by ENUMSET1:def_4; then ( x in {x1,x3,x6} or x in {x2,x4,x5} ) by ENUMSET1:def_1; hence x in {x1,x3,x6} \/ {x2,x4,x5} by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x1,x3,x6} \/ {x2,x4,x5} or x in {x1,x2,x3,x4,x5,x6} ) assume x in {x1,x3,x6} \/ {x2,x4,x5} ; ::_thesis: x in {x1,x2,x3,x4,x5,x6} then ( x in {x1,x3,x6} or x in {x2,x4,x5} ) by XBOOLE_0:def_3; then ( x = x1 or x = x3 or x = x6 or x = x2 or x = x4 or x = x5 ) by ENUMSET1:def_1; hence x in {x1,x2,x3,x4,x5,x6} by ENUMSET1:def_4; ::_thesis: verum end; theorem Th3: :: BORSUK_5:3 for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3,x4,x5,x6 are_mutually_different holds card {x1,x2,x3,x4,x5,x6} = 6 proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6 are_mutually_different implies card {x1,x2,x3,x4,x5,x6} = 6 ) A1: {x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6} by ENUMSET1:15; assume A2: x1,x2,x3,x4,x5,x6 are_mutually_different ; ::_thesis: card {x1,x2,x3,x4,x5,x6} = 6 then A3: x1 <> x3 by ZFMISC_1:def_8; A4: x4 <> x5 by A2, ZFMISC_1:def_8; A5: x3 <> x5 by A2, ZFMISC_1:def_8; A6: x3 <> x4 by A2, ZFMISC_1:def_8; A7: x2 <> x5 by A2, ZFMISC_1:def_8; A8: x2 <> x4 by A2, ZFMISC_1:def_8; A9: x2 <> x3 by A2, ZFMISC_1:def_8; A10: x1 <> x5 by A2, ZFMISC_1:def_8; A11: x1 <> x4 by A2, ZFMISC_1:def_8; x1 <> x2 by A2, ZFMISC_1:def_8; then x1,x2,x3,x4,x5 are_mutually_different by A3, A11, A10, A9, A8, A7, A6, A5, A4, ZFMISC_1:def_7; then A12: card {x1,x2,x3,x4,x5} = 5 by CARD_2:63; A13: x3 <> x6 by A2, ZFMISC_1:def_8; A14: x2 <> x6 by A2, ZFMISC_1:def_8; A15: x5 <> x6 by A2, ZFMISC_1:def_8; A16: x4 <> x6 by A2, ZFMISC_1:def_8; x1 <> x6 by A2, ZFMISC_1:def_8; then not x6 in {x1,x2,x3,x4,x5} by A14, A13, A16, A15, ENUMSET1:def_3; hence card {x1,x2,x3,x4,x5,x6} = 5 + 1 by A12, A1, CARD_2:41 .= 6 ; ::_thesis: verum end; theorem :: BORSUK_5:4 for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds card {x1,x2,x3,x4,x5,x6,x7} = 7 proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6,x7 are_mutually_different implies card {x1,x2,x3,x4,x5,x6,x7} = 7 ) A1: {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7} by ENUMSET1:21; assume A2: x1,x2,x3,x4,x5,x6,x7 are_mutually_different ; ::_thesis: card {x1,x2,x3,x4,x5,x6,x7} = 7 then A3: x1 <> x3 by ZFMISC_1:def_9; A4: x5 <> x7 by A2, ZFMISC_1:def_9; A5: x4 <> x7 by A2, ZFMISC_1:def_9; A6: x3 <> x7 by A2, ZFMISC_1:def_9; A7: x2 <> x7 by A2, ZFMISC_1:def_9; A8: x4 <> x6 by A2, ZFMISC_1:def_9; A9: x4 <> x5 by A2, ZFMISC_1:def_9; A10: x5 <> x6 by A2, ZFMISC_1:def_9; A11: x1 <> x5 by A2, ZFMISC_1:def_9; A12: x1 <> x4 by A2, ZFMISC_1:def_9; A13: x3 <> x6 by A2, ZFMISC_1:def_9; A14: x3 <> x5 by A2, ZFMISC_1:def_9; A15: x3 <> x4 by A2, ZFMISC_1:def_9; A16: x2 <> x6 by A2, ZFMISC_1:def_9; A17: x2 <> x5 by A2, ZFMISC_1:def_9; A18: x2 <> x4 by A2, ZFMISC_1:def_9; A19: x2 <> x3 by A2, ZFMISC_1:def_9; A20: x1 <> x6 by A2, ZFMISC_1:def_9; x1 <> x2 by A2, ZFMISC_1:def_9; then x1,x2,x3,x4,x5,x6 are_mutually_different by A3, A12, A11, A20, A19, A18, A17, A16, A15, A14, A13, A9, A8, A10, ZFMISC_1:def_8; then A21: card {x1,x2,x3,x4,x5,x6} = 6 by Th3; A22: x6 <> x7 by A2, ZFMISC_1:def_9; x1 <> x7 by A2, ZFMISC_1:def_9; then not x7 in {x1,x2,x3,x4,x5,x6} by A7, A6, A5, A4, A22, ENUMSET1:def_4; hence card {x1,x2,x3,x4,x5,x6,x7} = 6 + 1 by A21, A1, CARD_2:41 .= 7 ; ::_thesis: verum end; theorem Th5: :: BORSUK_5:5 for x1, x2, x3, x4, x5, x6 being set st {x1,x2,x3} misses {x4,x5,x6} holds ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 ) proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: ( {x1,x2,x3} misses {x4,x5,x6} implies ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 ) ) assume A1: {x1,x2,x3} misses {x4,x5,x6} ; ::_thesis: ( x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 ) A2: x5 in {x4,x5,x6} by ENUMSET1:def_1; assume ( x1 = x4 or x1 = x5 or x1 = x6 or x2 = x4 or x2 = x5 or x2 = x6 or x3 = x4 or x3 = x5 or x3 = x6 ) ; ::_thesis: contradiction then A3: ( x4 in {x1,x2,x3} or x5 in {x1,x2,x3} or x6 in {x1,x2,x3} ) by ENUMSET1:def_1; A4: x6 in {x4,x5,x6} by ENUMSET1:def_1; x4 in {x4,x5,x6} by ENUMSET1:def_1; hence contradiction by A1, A3, A2, A4, XBOOLE_0:3; ::_thesis: verum end; theorem :: BORSUK_5:6 for x1, x2, x3, x4, x5, x6 being set st x1,x2,x3 are_mutually_different & x4,x5,x6 are_mutually_different & {x1,x2,x3} misses {x4,x5,x6} holds x1,x2,x3,x4,x5,x6 are_mutually_different proof let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: ( x1,x2,x3 are_mutually_different & x4,x5,x6 are_mutually_different & {x1,x2,x3} misses {x4,x5,x6} implies x1,x2,x3,x4,x5,x6 are_mutually_different ) assume that A1: x1,x2,x3 are_mutually_different and A2: x4,x5,x6 are_mutually_different and A3: {x1,x2,x3} misses {x4,x5,x6} ; ::_thesis: x1,x2,x3,x4,x5,x6 are_mutually_different A4: x1 <> x2 by A1, ZFMISC_1:def_5; A5: x3 <> x5 by A3, Th5; A6: x3 <> x4 by A3, Th5; A7: x1 <> x6 by A3, Th5; A8: x1 <> x3 by A1, ZFMISC_1:def_5; A9: x2 <> x5 by A3, Th5; A10: x5 <> x6 by A2, ZFMISC_1:def_5; A11: x2 <> x4 by A3, Th5; A12: x4 <> x5 by A2, ZFMISC_1:def_5; A13: x2 <> x6 by A3, Th5; A14: x4 <> x6 by A2, ZFMISC_1:def_5; A15: x3 <> x6 by A3, Th5; A16: x1 <> x5 by A3, Th5; A17: x2 <> x3 by A1, ZFMISC_1:def_5; x1 <> x4 by A3, Th5; hence x1,x2,x3,x4,x5,x6 are_mutually_different by A4, A17, A8, A12, A10, A14, A16, A7, A11, A9, A13, A6, A5, A15, ZFMISC_1:def_8; ::_thesis: verum end; theorem :: BORSUK_5:7 for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6 are_mutually_different & {x1,x2,x3,x4,x5,x6} misses {x7} holds x1,x2,x3,x4,x5,x6,x7 are_mutually_different proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6 are_mutually_different & {x1,x2,x3,x4,x5,x6} misses {x7} implies x1,x2,x3,x4,x5,x6,x7 are_mutually_different ) assume that A1: x1,x2,x3,x4,x5,x6 are_mutually_different and A2: {x1,x2,x3,x4,x5,x6} misses {x7} ; ::_thesis: x1,x2,x3,x4,x5,x6,x7 are_mutually_different A3: x1 <> x3 by A1, ZFMISC_1:def_8; A4: x2 <> x3 by A1, ZFMISC_1:def_8; A5: x1 <> x6 by A1, ZFMISC_1:def_8; A6: x1 <> x5 by A1, ZFMISC_1:def_8; A7: x1 <> x4 by A1, ZFMISC_1:def_8; A8: not x7 in {x1,x2,x3,x4,x5,x6} by A2, ZFMISC_1:48; then A9: x7 <> x1 by ENUMSET1:def_4; A10: x4 <> x6 by A1, ZFMISC_1:def_8; A11: x4 <> x5 by A1, ZFMISC_1:def_8; A12: x3 <> x6 by A1, ZFMISC_1:def_8; A13: x3 <> x5 by A1, ZFMISC_1:def_8; A14: x3 <> x4 by A1, ZFMISC_1:def_8; A15: x2 <> x6 by A1, ZFMISC_1:def_8; A16: x2 <> x5 by A1, ZFMISC_1:def_8; A17: x2 <> x4 by A1, ZFMISC_1:def_8; A18: x7 <> x6 by A8, ENUMSET1:def_4; A19: x5 <> x6 by A1, ZFMISC_1:def_8; A20: x7 <> x5 by A8, ENUMSET1:def_4; A21: x7 <> x4 by A8, ENUMSET1:def_4; A22: x7 <> x3 by A8, ENUMSET1:def_4; A23: x7 <> x2 by A8, ENUMSET1:def_4; x1 <> x2 by A1, ZFMISC_1:def_8; hence x1,x2,x3,x4,x5,x6,x7 are_mutually_different by A3, A7, A6, A5, A4, A17, A16, A15, A14, A13, A12, A11, A10, A19, A9, A23, A22, A21, A20, A18, ZFMISC_1:def_9; ::_thesis: verum end; theorem :: BORSUK_5:8 for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds x7,x1,x2,x3,x4,x5,x6 are_mutually_different proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6,x7 are_mutually_different implies x7,x1,x2,x3,x4,x5,x6 are_mutually_different ) assume A1: x1,x2,x3,x4,x5,x6,x7 are_mutually_different ; ::_thesis: x7,x1,x2,x3,x4,x5,x6 are_mutually_different then A2: x1 <> x3 by ZFMISC_1:def_9; A3: x5 <> x7 by A1, ZFMISC_1:def_9; A4: x5 <> x6 by A1, ZFMISC_1:def_9; A5: x4 <> x7 by A1, ZFMISC_1:def_9; A6: x4 <> x6 by A1, ZFMISC_1:def_9; A7: x6 <> x7 by A1, ZFMISC_1:def_9; A8: x1 <> x5 by A1, ZFMISC_1:def_9; A9: x1 <> x4 by A1, ZFMISC_1:def_9; A10: x2 <> x4 by A1, ZFMISC_1:def_9; A11: x2 <> x3 by A1, ZFMISC_1:def_9; A12: x1 <> x7 by A1, ZFMISC_1:def_9; A13: x1 <> x6 by A1, ZFMISC_1:def_9; A14: x4 <> x5 by A1, ZFMISC_1:def_9; A15: x3 <> x7 by A1, ZFMISC_1:def_9; A16: x3 <> x6 by A1, ZFMISC_1:def_9; A17: x3 <> x5 by A1, ZFMISC_1:def_9; A18: x3 <> x4 by A1, ZFMISC_1:def_9; A19: x2 <> x7 by A1, ZFMISC_1:def_9; A20: x2 <> x6 by A1, ZFMISC_1:def_9; A21: x2 <> x5 by A1, ZFMISC_1:def_9; x1 <> x2 by A1, ZFMISC_1:def_9; hence x7,x1,x2,x3,x4,x5,x6 are_mutually_different by A2, A9, A8, A13, A12, A11, A10, A21, A20, A19, A18, A17, A16, A15, A14, A6, A5, A4, A3, A7, ZFMISC_1:def_9; ::_thesis: verum end; theorem :: BORSUK_5:9 for x1, x2, x3, x4, x5, x6, x7 being set st x1,x2,x3,x4,x5,x6,x7 are_mutually_different holds x1,x2,x5,x3,x6,x7,x4 are_mutually_different proof let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: ( x1,x2,x3,x4,x5,x6,x7 are_mutually_different implies x1,x2,x5,x3,x6,x7,x4 are_mutually_different ) assume A1: x1,x2,x3,x4,x5,x6,x7 are_mutually_different ; ::_thesis: x1,x2,x5,x3,x6,x7,x4 are_mutually_different then A2: x1 <> x3 by ZFMISC_1:def_9; A3: x5 <> x7 by A1, ZFMISC_1:def_9; A4: x5 <> x6 by A1, ZFMISC_1:def_9; A5: x4 <> x7 by A1, ZFMISC_1:def_9; A6: x4 <> x6 by A1, ZFMISC_1:def_9; A7: x6 <> x7 by A1, ZFMISC_1:def_9; A8: x1 <> x5 by A1, ZFMISC_1:def_9; A9: x1 <> x4 by A1, ZFMISC_1:def_9; A10: x2 <> x4 by A1, ZFMISC_1:def_9; A11: x2 <> x3 by A1, ZFMISC_1:def_9; A12: x1 <> x7 by A1, ZFMISC_1:def_9; A13: x1 <> x6 by A1, ZFMISC_1:def_9; A14: x4 <> x5 by A1, ZFMISC_1:def_9; A15: x3 <> x7 by A1, ZFMISC_1:def_9; A16: x3 <> x6 by A1, ZFMISC_1:def_9; A17: x3 <> x5 by A1, ZFMISC_1:def_9; A18: x3 <> x4 by A1, ZFMISC_1:def_9; A19: x2 <> x7 by A1, ZFMISC_1:def_9; A20: x2 <> x6 by A1, ZFMISC_1:def_9; A21: x2 <> x5 by A1, ZFMISC_1:def_9; x1 <> x2 by A1, ZFMISC_1:def_9; hence x1,x2,x5,x3,x6,x7,x4 are_mutually_different by A2, A9, A8, A13, A12, A11, A10, A21, A20, A19, A18, A17, A16, A15, A14, A6, A5, A4, A3, A7, ZFMISC_1:def_9; ::_thesis: verum end; Lm1: R^1 is pathwise_connected proof let a, b be Point of R^1; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected percases ( a <= b or b <= a ) ; supposeA1: a <= b ; ::_thesis: a,b are_connected reconsider B = [.a,b.] as Subset of R^1 by TOPMETR:17; reconsider B = B as non empty Subset of R^1 by A1, XXREAL_1:1; A2: Closed-Interval-TSpace (a,b) = R^1 | B by A1, TOPMETR:19; the carrier of (R^1 | B) c= the carrier of R^1 by BORSUK_1:1; then reconsider g = L[01] (((#) (a,b)),((a,b) (#))) as Function of the carrier of I[01], the carrier of R^1 by A2, FUNCT_2:7, TOPMETR:20; reconsider g = g as Function of I[01],R^1 ; take g ; :: according to BORSUK_2:def_1 ::_thesis: ( g is continuous & g . 0 = a & g . 1 = b ) L[01] (((#) (a,b)),((a,b) (#))) is continuous Function of I[01],(R^1 | B) by A1, A2, TOPMETR:20, TREAL_1:8; hence g is continuous by PRE_TOPC:26; ::_thesis: ( g . 0 = a & g . 1 = b ) 0 = (#) (0,1) by TREAL_1:def_1; hence g . 0 = (#) (a,b) by A1, TREAL_1:9 .= a by A1, TREAL_1:def_1 ; ::_thesis: g . 1 = b 1 = (0,1) (#) by TREAL_1:def_2; hence g . 1 = (a,b) (#) by A1, TREAL_1:9 .= b by A1, TREAL_1:def_2 ; ::_thesis: verum end; supposeA3: b <= a ; ::_thesis: a,b are_connected reconsider B = [.b,a.] as Subset of R^1 by TOPMETR:17; b in B by A3, XXREAL_1:1; then reconsider B = [.b,a.] as non empty Subset of R^1 ; A4: Closed-Interval-TSpace (b,a) = R^1 | B by A3, TOPMETR:19; the carrier of (R^1 | B) c= the carrier of R^1 by BORSUK_1:1; then reconsider g = L[01] (((#) (b,a)),((b,a) (#))) as Function of the carrier of I[01], the carrier of R^1 by A4, FUNCT_2:7, TOPMETR:20; reconsider g = g as Function of I[01],R^1 ; 0 = (#) (0,1) by TREAL_1:def_1; then A5: g . 0 = (#) (b,a) by A3, TREAL_1:9 .= b by A3, TREAL_1:def_1 ; 1 = (0,1) (#) by TREAL_1:def_2; then A6: g . 1 = (b,a) (#) by A3, TREAL_1:9 .= a by A3, TREAL_1:def_2 ; L[01] (((#) (b,a)),((b,a) (#))) is continuous Function of I[01],(R^1 | B) by A3, A4, TOPMETR:20, TREAL_1:8; then A7: g is continuous by PRE_TOPC:26; then b,a are_connected by A5, A6, BORSUK_2:def_1; then reconsider P = g as Path of b,a by A7, A5, A6, BORSUK_2:def_2; take - P ; :: according to BORSUK_2:def_1 ::_thesis: ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b ) ex t being Function of I[01],R^1 st ( t is continuous & t . 0 = a & t . 1 = b ) by A7, A5, A6, BORSUK_2:15; then a,b are_connected by BORSUK_2:def_1; hence ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b ) by BORSUK_2:def_2; ::_thesis: verum end; end; end; registration cluster R^1 -> pathwise_connected ; coherence R^1 is pathwise_connected by Lm1; end; registration cluster non empty TopSpace-like connected for TopStruct ; existence ex b1 being TopSpace st ( b1 is connected & not b1 is empty ) proof take R^1 ; ::_thesis: ( R^1 is connected & not R^1 is empty ) thus ( R^1 is connected & not R^1 is empty ) ; ::_thesis: verum end; end; begin theorem :: BORSUK_5:10 for A, B being Subset of R^1 for a, b, c, d being real number st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds A,B are_separated proof let A, B be Subset of R^1; ::_thesis: for a, b, c, d being real number st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds A,B are_separated let a, b, c, d be real number ; ::_thesis: ( a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] implies A,B are_separated ) assume that A1: a < b and A2: b <= c and A3: c < d and A4: A = [.a,b.[ and A5: B = ].c,d.] ; ::_thesis: A,B are_separated Cl ].c,d.] = [.c,d.] by A3, BORSUK_4:11; then Cl B = [.c,d.] by A5, JORDAN5A:24; then A6: Cl B misses A by A2, A4, XXREAL_1:95; Cl [.a,b.[ = [.a,b.] by A1, BORSUK_4:12; then Cl A = [.a,b.] by A4, JORDAN5A:24; then Cl A misses B by A2, A5, XXREAL_1:90; hence A,B are_separated by A6, CONNSP_1:def_1; ::_thesis: verum end; theorem Th11: :: BORSUK_5:11 for a, b, c being real number st a <= c & c <= b holds [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ proof let a, b, c be real number ; ::_thesis: ( a <= c & c <= b implies [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ ) assume that A1: a <= c and A2: c <= b ; ::_thesis: [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ A3: [.a,+infty.[ c= [.a,b.] \/ [.c,+infty.[ proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in [.a,+infty.[ or r in [.a,b.] \/ [.c,+infty.[ ) assume A4: r in [.a,+infty.[ ; ::_thesis: r in [.a,b.] \/ [.c,+infty.[ then reconsider s = r as Real ; A5: a <= s by A4, XXREAL_1:236; percases ( s <= b or not s <= b ) ; suppose s <= b ; ::_thesis: r in [.a,b.] \/ [.c,+infty.[ then s in [.a,b.] by A5, XXREAL_1:1; hence r in [.a,b.] \/ [.c,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; suppose not s <= b ; ::_thesis: r in [.a,b.] \/ [.c,+infty.[ then c <= s by A2, XXREAL_0:2; then s in [.c,+infty.[ by XXREAL_1:236; hence r in [.a,b.] \/ [.c,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; end; end; A6: [.a,b.] c= right_closed_halfline a by XXREAL_1:251; [.c,+infty.[ c= [.a,+infty.[ by A1, XXREAL_1:38; then [.a,b.] \/ [.c,+infty.[ c= [.a,+infty.[ by A6, XBOOLE_1:8; hence [.a,b.] \/ [.c,+infty.[ = [.a,+infty.[ by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th12: :: BORSUK_5:12 for a, b, c being real number st a <= c & c <= b holds ].-infty,c.] \/ [.a,b.] = ].-infty,b.] proof let a, b, c be real number ; ::_thesis: ( a <= c & c <= b implies ].-infty,c.] \/ [.a,b.] = ].-infty,b.] ) assume that A1: a <= c and A2: c <= b ; ::_thesis: ].-infty,c.] \/ [.a,b.] = ].-infty,b.] thus ].-infty,c.] \/ [.a,b.] c= ].-infty,b.] :: according to XBOOLE_0:def_10 ::_thesis: ].-infty,b.] c= ].-infty,c.] \/ [.a,b.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,c.] \/ [.a,b.] or x in ].-infty,b.] ) assume A3: x in ].-infty,c.] \/ [.a,b.] ; ::_thesis: x in ].-infty,b.] then reconsider x = x as real number ; percases ( x in ].-infty,c.] or x in [.a,b.] ) by A3, XBOOLE_0:def_3; suppose x in ].-infty,c.] ; ::_thesis: x in ].-infty,b.] then x <= c by XXREAL_1:234; then x <= b by A2, XXREAL_0:2; hence x in ].-infty,b.] by XXREAL_1:234; ::_thesis: verum end; suppose x in [.a,b.] ; ::_thesis: x in ].-infty,b.] then x <= b by XXREAL_1:1; hence x in ].-infty,b.] by XXREAL_1:234; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,b.] or x in ].-infty,c.] \/ [.a,b.] ) assume A4: x in ].-infty,b.] ; ::_thesis: x in ].-infty,c.] \/ [.a,b.] then reconsider x = x as real number ; percases ( x <= c or x > c ) ; suppose x <= c ; ::_thesis: x in ].-infty,c.] \/ [.a,b.] then x in ].-infty,c.] by XXREAL_1:234; hence x in ].-infty,c.] \/ [.a,b.] by XBOOLE_0:def_3; ::_thesis: verum end; supposeA5: x > c ; ::_thesis: x in ].-infty,c.] \/ [.a,b.] A6: x <= b by A4, XXREAL_1:234; x > a by A1, A5, XXREAL_0:2; then x in [.a,b.] by A6, XXREAL_1:1; hence x in ].-infty,c.] \/ [.a,b.] by XBOOLE_0:def_3; ::_thesis: verum end; end; end; registration cluster -> real for Element of RAT ; coherence for b1 being Element of RAT holds b1 is real ; end; theorem :: BORSUK_5:13 for A being Subset of R^1 for p being Point of RealSpace holds ( p in Cl A iff for r being real number st r > 0 holds Ball (p,r) meets A ) by GOBOARD6:92, TOPMETR:def_6; theorem Th14: :: BORSUK_5:14 for p, q being Element of RealSpace st q >= p holds dist (p,q) = q - p proof let p, q be Element of RealSpace; ::_thesis: ( q >= p implies dist (p,q) = q - p ) assume p <= q ; ::_thesis: dist (p,q) = q - p then A1: q - p >= 0 by XREAL_1:48; dist (p,q) = abs (q - p) by TOPMETR:11 .= q - p by A1, ABSVALUE:def_1 ; hence dist (p,q) = q - p ; ::_thesis: verum end; theorem Th15: :: BORSUK_5:15 for A being Subset of R^1 st A = RAT holds Cl A = the carrier of R^1 proof let A be Subset of R^1; ::_thesis: ( A = RAT implies Cl A = the carrier of R^1 ) assume A1: A = RAT ; ::_thesis: Cl A = the carrier of R^1 the carrier of R^1 c= Cl A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R^1 or x in Cl A ) assume x in the carrier of R^1 ; ::_thesis: x in Cl A then reconsider p = x as Element of RealSpace by METRIC_1:def_13, TOPMETR:17; now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_ Ball_(p,r)_meets_A let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A ) reconsider pr = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; assume r > 0 ; ::_thesis: Ball (p,r) meets A then consider Q being rational number such that A2: p < Q and A3: Q < pr by RAT_1:7, XREAL_1:29; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; P - p < pr - p by A3, XREAL_1:9; then dist (p,P) < r by A2, Th14; then A4: P in Ball (p,r) by METRIC_1:11; Q in A by A1, RAT_1:def_2; hence Ball (p,r) meets A by A4, XBOOLE_0:3; ::_thesis: verum end; hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; hence Cl A = the carrier of R^1 by XBOOLE_0:def_10; ::_thesis: verum end; theorem Th16: :: BORSUK_5:16 for A being Subset of R^1 for a, b being real number st A = ].a,b.[ & a <> b holds Cl A = [.a,b.] proof let A be Subset of R^1; ::_thesis: for a, b being real number st A = ].a,b.[ & a <> b holds Cl A = [.a,b.] let a, b be real number ; ::_thesis: ( A = ].a,b.[ & a <> b implies Cl A = [.a,b.] ) assume that A1: A = ].a,b.[ and A2: a <> b ; ::_thesis: Cl A = [.a,b.] Cl ].a,b.[ = [.a,b.] by A2, JORDAN5A:26; hence Cl A = [.a,b.] by A1, JORDAN5A:24; ::_thesis: verum end; begin registration cluster number_e -> irrational ; coherence number_e is irrational by IRRAT_1:41; end; definition func IRRAT -> Subset of REAL equals :: BORSUK_5:def 1 REAL \ RAT; coherence REAL \ RAT is Subset of REAL ; end; :: deftheorem defines IRRAT BORSUK_5:def_1_:_ IRRAT = REAL \ RAT; definition let a, b be real number ; func RAT (a,b) -> Subset of REAL equals :: BORSUK_5:def 2 RAT /\ ].a,b.[; coherence RAT /\ ].a,b.[ is Subset of REAL ; func IRRAT (a,b) -> Subset of REAL equals :: BORSUK_5:def 3 IRRAT /\ ].a,b.[; coherence IRRAT /\ ].a,b.[ is Subset of REAL ; end; :: deftheorem defines RAT BORSUK_5:def_2_:_ for a, b being real number holds RAT (a,b) = RAT /\ ].a,b.[; :: deftheorem defines IRRAT BORSUK_5:def_3_:_ for a, b being real number holds IRRAT (a,b) = IRRAT /\ ].a,b.[; theorem Th17: :: BORSUK_5:17 for x being real number holds ( x is irrational iff x in IRRAT ) proof let x be real number ; ::_thesis: ( x is irrational iff x in IRRAT ) A1: x in REAL by XREAL_0:def_1; hereby ::_thesis: ( x in IRRAT implies x is irrational ) assume x is irrational ; ::_thesis: x in IRRAT then not x in RAT ; hence x in IRRAT by A1, XBOOLE_0:def_5; ::_thesis: verum end; assume x in IRRAT ; ::_thesis: x is irrational then not x in RAT by XBOOLE_0:def_5; hence x is irrational by RAT_1:def_2; ::_thesis: verum end; registration cluster complex real ext-real irrational for set ; existence ex b1 being real number st b1 is irrational by IRRAT_1:41; end; registration cluster IRRAT -> non empty ; coherence not IRRAT is empty by Th17, IRRAT_1:41; end; registration let a be rational number ; let b be real irrational number ; clustera + b -> irrational ; coherence a + b is irrational proof set m1 = the Integer; assume a + b is rational ; ::_thesis: contradiction then consider m, n being Integer such that n <> 0 and A1: a + b = m / n by RAT_1:2; (a + b) - a = ((m * the Integer) - ( the Integer * n)) / ( the Integer * n) by A1; hence contradiction ; ::_thesis: verum end; clusterb + a -> irrational ; coherence b + a is irrational ; end; theorem :: BORSUK_5:18 for a being rational number for b being real irrational number holds a + b is irrational ; registration let a be real irrational number ; cluster - a -> irrational ; coherence - a is irrational proof assume - a is rational ; ::_thesis: contradiction then reconsider b = - a as rational number ; - b is rational ; hence contradiction ; ::_thesis: verum end; end; theorem :: BORSUK_5:19 for a being real irrational number holds - a is irrational ; registration let a be rational number ; let b be real irrational number ; clustera - b -> irrational ; coherence a - b is irrational proof a + (- b) is irrational ; hence a - b is irrational ; ::_thesis: verum end; clusterb - a -> irrational ; coherence b - a is irrational proof b + (- a) is irrational ; hence b - a is irrational ; ::_thesis: verum end; end; theorem :: BORSUK_5:20 for a being rational number for b being real irrational number holds a - b is irrational ; theorem :: BORSUK_5:21 for a being rational number for b being real irrational number holds b - a is irrational ; theorem Th22: :: BORSUK_5:22 for a being rational number for b being real irrational number st a <> 0 holds a * b is irrational proof let a be rational number ; ::_thesis: for b being real irrational number st a <> 0 holds a * b is irrational let b be real irrational number ; ::_thesis: ( a <> 0 implies a * b is irrational ) assume A1: a <> 0 ; ::_thesis: a * b is irrational assume a * b is rational ; ::_thesis: contradiction then consider m, n being Integer such that n <> 0 and A2: a * b = m / n by RAT_1:2; consider m1, n1 being Integer such that n1 <> 0 and A3: a = m1 / n1 by RAT_1:2; (a * b) / a = (m * n1) / (n * m1) by A2, A3, XCMPLX_1:84; hence contradiction by A1, XCMPLX_1:89; ::_thesis: verum end; theorem Th23: :: BORSUK_5:23 for a being rational number for b being real irrational number st a <> 0 holds b / a is irrational proof let a be rational number ; ::_thesis: for b being real irrational number st a <> 0 holds b / a is irrational let b be real irrational number ; ::_thesis: ( a <> 0 implies b / a is irrational ) assume A1: a <> 0 ; ::_thesis: b / a is irrational assume b / a is rational ; ::_thesis: contradiction then reconsider c = b / a as rational number ; c * a is rational ; hence contradiction by A1, XCMPLX_1:87; ::_thesis: verum end; registration cluster real irrational -> non zero real for set ; coherence for b1 being real number st b1 is irrational holds not b1 is zero proof let a be real number ; ::_thesis: ( a is irrational implies not a is zero ) assume A1: a is irrational ; ::_thesis: not a is zero assume a is zero ; ::_thesis: contradiction then a = 0 / 1 ; hence contradiction by A1; ::_thesis: verum end; end; theorem Th24: :: BORSUK_5:24 for a being rational number for b being real irrational number st a <> 0 holds a / b is irrational proof let a be rational number ; ::_thesis: for b being real irrational number st a <> 0 holds a / b is irrational let b be real irrational number ; ::_thesis: ( a <> 0 implies a / b is irrational ) assume A1: a <> 0 ; ::_thesis: a / b is irrational assume a / b is rational ; ::_thesis: contradiction then reconsider c = a / b as rational number ; c * b is irrational by A1, Th22, XCMPLX_1:50; hence contradiction by XCMPLX_1:87; ::_thesis: verum end; registration let r be real irrational number ; cluster frac r -> irrational ; coherence frac r is irrational proof frac r = r - [\r/] by INT_1:def_8; hence frac r is irrational ; ::_thesis: verum end; end; theorem :: BORSUK_5:25 for r being real irrational number holds frac r is irrational ; registration cluster non zero complex real ext-real rational for set ; existence not for b1 being rational number holds b1 is zero proof 1 <> 0 ; hence not for b1 being rational number holds b1 is zero ; ::_thesis: verum end; end; registration let a be non zero rational number ; let b be real irrational number ; clustera * b -> irrational ; coherence a * b is irrational by Th22; clusterb * a -> irrational ; coherence b * a is irrational ; clustera / b -> irrational ; coherence a / b is irrational by Th24; clusterb / a -> irrational ; coherence b / a is irrational by Th23; end; theorem Th26: :: BORSUK_5:26 for a, b being real number st a < b holds ex p1, p2 being rational number st ( a < p1 & p1 < p2 & p2 < b ) proof let a, b be real number ; ::_thesis: ( a < b implies ex p1, p2 being rational number st ( a < p1 & p1 < p2 & p2 < b ) ) assume a < b ; ::_thesis: ex p1, p2 being rational number st ( a < p1 & p1 < p2 & p2 < b ) then consider p1 being rational number such that A1: a < p1 and A2: p1 < b by RAT_1:7; ex p2 being rational number st ( p1 < p2 & p2 < b ) by A2, RAT_1:7; hence ex p1, p2 being rational number st ( a < p1 & p1 < p2 & p2 < b ) by A1; ::_thesis: verum end; theorem Th27: :: BORSUK_5:27 for a, b being real number st a < b holds ex p being real irrational number st ( a < p & p < b ) proof set x = frac number_e; let a, b be real number ; ::_thesis: ( a < b implies ex p being real irrational number st ( a < p & p < b ) ) A1: frac number_e < 1 by INT_1:43; assume a < b ; ::_thesis: ex p being real irrational number st ( a < p & p < b ) then consider p1, p2 being rational number such that A2: a < p1 and A3: p1 < p2 and A4: p2 < b by Th26; set y = ((1 - (frac number_e)) * p1) + ((frac number_e) * p2); A5: 0 < frac number_e by INT_1:43; then ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) < p2 by A3, A1, XREAL_1:178; then A6: ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) < b by A4, XXREAL_0:2; ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) > p1 by A3, A5, A1, XREAL_1:177; then A7: ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) > a by A2, XXREAL_0:2; A8: ((1 - (frac number_e)) * p1) + ((frac number_e) * p2) = p1 + ((frac number_e) * (p2 - p1)) ; p2 - p1 <> 0 by A3; hence ex p being real irrational number st ( a < p & p < b ) by A8, A6, A7; ::_thesis: verum end; theorem Th28: :: BORSUK_5:28 for A being Subset of R^1 st A = IRRAT holds Cl A = the carrier of R^1 proof let A be Subset of R^1; ::_thesis: ( A = IRRAT implies Cl A = the carrier of R^1 ) assume A1: A = IRRAT ; ::_thesis: Cl A = the carrier of R^1 the carrier of R^1 c= Cl A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of R^1 or x in Cl A ) assume x in the carrier of R^1 ; ::_thesis: x in Cl A then reconsider p = x as Element of RealSpace by METRIC_1:def_13, TOPMETR:17; now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_ Ball_(p,r)_meets_A let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A ) reconsider pr = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; assume r > 0 ; ::_thesis: Ball (p,r) meets A then consider Q being real irrational number such that A2: p < Q and A3: Q < pr by Th27, XREAL_1:29; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; P - p < pr - p by A3, XREAL_1:9; then dist (p,P) < r by A2, Th14; then A4: P in Ball (p,r) by METRIC_1:11; Q in A by A1, Th17; hence Ball (p,r) meets A by A4, XBOOLE_0:3; ::_thesis: verum end; hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; hence Cl A = the carrier of R^1 by XBOOLE_0:def_10; ::_thesis: verum end; Lm2: for A being Subset of R^1 for a, b being real number st a < b & A = RAT (a,b) holds ( a in Cl A & b in Cl A ) proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = RAT (a,b) holds ( a in Cl A & b in Cl A ) let a, b be real number ; ::_thesis: ( a < b & A = RAT (a,b) implies ( a in Cl A & b in Cl A ) ) assume that A1: a < b and A2: A = RAT (a,b) ; ::_thesis: ( a in Cl A & b in Cl A ) thus a in Cl A ::_thesis: b in Cl A proof reconsider a9 = a as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; for r being real number st r > 0 holds Ball (a9,r) meets A proof set p = a; let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A ) reconsider pp = a + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; set pr = min (pp,((a + b) / 2)); A3: min (pp,((a + b) / 2)) <= (a + b) / 2 by XXREAL_0:17; assume A4: r > 0 ; ::_thesis: Ball (a9,r) meets A a < min (pp,((a + b) / 2)) proof percases ( min (pp,((a + b) / 2)) = pp or min (pp,((a + b) / 2)) = (a + b) / 2 ) by XXREAL_0:15; suppose min (pp,((a + b) / 2)) = pp ; ::_thesis: a < min (pp,((a + b) / 2)) hence a < min (pp,((a + b) / 2)) by A4, XREAL_1:29; ::_thesis: verum end; suppose min (pp,((a + b) / 2)) = (a + b) / 2 ; ::_thesis: a < min (pp,((a + b) / 2)) hence a < min (pp,((a + b) / 2)) by A1, XREAL_1:226; ::_thesis: verum end; end; end; then consider Q being rational number such that A5: a < Q and A6: Q < min (pp,((a + b) / 2)) by RAT_1:7; (a + b) / 2 < b by A1, XREAL_1:226; then min (pp,((a + b) / 2)) < b by A3, XXREAL_0:2; then Q < b by A6, XXREAL_0:2; then A7: Q in ].a,b.[ by A5, XXREAL_1:4; min (pp,((a + b) / 2)) <= pp by XXREAL_0:17; then A8: (min (pp,((a + b) / 2))) - a <= pp - a by XREAL_1:9; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; P - a < (min (pp,((a + b) / 2))) - a by A6, XREAL_1:9; then P - a < r by A8, XXREAL_0:2; then dist (a9,P) < r by A5, Th14; then A9: P in Ball (a9,r) by METRIC_1:11; Q in RAT by RAT_1:def_2; then Q in A by A2, A7, XBOOLE_0:def_4; hence Ball (a9,r) meets A by A9, XBOOLE_0:3; ::_thesis: verum end; hence a in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; b in Cl A proof reconsider a9 = b as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; for r being real number st r > 0 holds Ball (a9,r) meets A proof set p = b; let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A ) reconsider pp = b - r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; set pr = max (pp,((b + a) / 2)); A10: max (pp,((b + a) / 2)) >= (b + a) / 2 by XXREAL_0:25; assume r > 0 ; ::_thesis: Ball (a9,r) meets A then A11: b < b + r by XREAL_1:29; b > max (pp,((b + a) / 2)) proof percases ( max (pp,((b + a) / 2)) = pp or max (pp,((b + a) / 2)) = (b + a) / 2 ) by XXREAL_0:16; suppose max (pp,((b + a) / 2)) = pp ; ::_thesis: b > max (pp,((b + a) / 2)) hence b > max (pp,((b + a) / 2)) by A11, XREAL_1:19; ::_thesis: verum end; suppose max (pp,((b + a) / 2)) = (b + a) / 2 ; ::_thesis: b > max (pp,((b + a) / 2)) hence b > max (pp,((b + a) / 2)) by A1, XREAL_1:226; ::_thesis: verum end; end; end; then consider Q being rational number such that A12: max (pp,((b + a) / 2)) < Q and A13: Q < b by RAT_1:7; (b + a) / 2 > a by A1, XREAL_1:226; then a < max (pp,((b + a) / 2)) by A10, XXREAL_0:2; then a < Q by A12, XXREAL_0:2; then A14: Q in ].a,b.[ by A13, XXREAL_1:4; max (pp,((b + a) / 2)) >= pp by XXREAL_0:25; then A15: b - (max (pp,((b + a) / 2))) <= b - pp by XREAL_1:13; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; b - P < b - (max (pp,((b + a) / 2))) by A12, XREAL_1:10; then b - P < r by A15, XXREAL_0:2; then dist (a9,P) < r by A13, Th14; then A16: P in Ball (a9,r) by METRIC_1:11; Q in RAT by RAT_1:def_2; then Q in A by A2, A14, XBOOLE_0:def_4; hence Ball (a9,r) meets A by A16, XBOOLE_0:3; ::_thesis: verum end; hence b in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; hence b in Cl A ; ::_thesis: verum end; Lm3: for A being Subset of R^1 for a, b being real number st a < b & A = IRRAT (a,b) holds ( a in Cl A & b in Cl A ) proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = IRRAT (a,b) holds ( a in Cl A & b in Cl A ) let a, b be real number ; ::_thesis: ( a < b & A = IRRAT (a,b) implies ( a in Cl A & b in Cl A ) ) assume that A1: a < b and A2: A = IRRAT (a,b) ; ::_thesis: ( a in Cl A & b in Cl A ) thus a in Cl A ::_thesis: b in Cl A proof reconsider a9 = a as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; for r being real number st r > 0 holds Ball (a9,r) meets A proof set p = a; let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A ) reconsider pp = a + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; set pr = min (pp,((a + b) / 2)); A3: min (pp,((a + b) / 2)) <= (a + b) / 2 by XXREAL_0:17; assume A4: r > 0 ; ::_thesis: Ball (a9,r) meets A a < min (pp,((a + b) / 2)) proof percases ( min (pp,((a + b) / 2)) = pp or min (pp,((a + b) / 2)) = (a + b) / 2 ) by XXREAL_0:15; suppose min (pp,((a + b) / 2)) = pp ; ::_thesis: a < min (pp,((a + b) / 2)) hence a < min (pp,((a + b) / 2)) by A4, XREAL_1:29; ::_thesis: verum end; suppose min (pp,((a + b) / 2)) = (a + b) / 2 ; ::_thesis: a < min (pp,((a + b) / 2)) hence a < min (pp,((a + b) / 2)) by A1, XREAL_1:226; ::_thesis: verum end; end; end; then consider Q being real irrational number such that A5: a < Q and A6: Q < min (pp,((a + b) / 2)) by Th27; (a + b) / 2 < b by A1, XREAL_1:226; then min (pp,((a + b) / 2)) < b by A3, XXREAL_0:2; then Q < b by A6, XXREAL_0:2; then A7: Q in ].a,b.[ by A5, XXREAL_1:4; min (pp,((a + b) / 2)) <= pp by XXREAL_0:17; then A8: (min (pp,((a + b) / 2))) - a <= pp - a by XREAL_1:9; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; P - a < (min (pp,((a + b) / 2))) - a by A6, XREAL_1:9; then P - a < r by A8, XXREAL_0:2; then dist (a9,P) < r by A5, Th14; then A9: P in Ball (a9,r) by METRIC_1:11; Q in IRRAT by Th17; then Q in A by A2, A7, XBOOLE_0:def_4; hence Ball (a9,r) meets A by A9, XBOOLE_0:3; ::_thesis: verum end; hence a in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; b in Cl A proof reconsider a9 = b as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; for r being real number st r > 0 holds Ball (a9,r) meets A proof set p = b; let r be real number ; ::_thesis: ( r > 0 implies Ball (a9,r) meets A ) reconsider pp = b - r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; set pr = max (pp,((b + a) / 2)); A10: max (pp,((b + a) / 2)) >= (b + a) / 2 by XXREAL_0:25; assume r > 0 ; ::_thesis: Ball (a9,r) meets A then A11: b < b + r by XREAL_1:29; b > max (pp,((b + a) / 2)) proof percases ( max (pp,((b + a) / 2)) = pp or max (pp,((b + a) / 2)) = (b + a) / 2 ) by XXREAL_0:16; suppose max (pp,((b + a) / 2)) = pp ; ::_thesis: b > max (pp,((b + a) / 2)) hence b > max (pp,((b + a) / 2)) by A11, XREAL_1:19; ::_thesis: verum end; suppose max (pp,((b + a) / 2)) = (b + a) / 2 ; ::_thesis: b > max (pp,((b + a) / 2)) hence b > max (pp,((b + a) / 2)) by A1, XREAL_1:226; ::_thesis: verum end; end; end; then consider Q being real irrational number such that A12: max (pp,((b + a) / 2)) < Q and A13: Q < b by Th27; (b + a) / 2 > a by A1, XREAL_1:226; then a < max (pp,((b + a) / 2)) by A10, XXREAL_0:2; then a < Q by A12, XXREAL_0:2; then A14: Q in ].a,b.[ by A13, XXREAL_1:4; max (pp,((b + a) / 2)) >= pp by XXREAL_0:25; then A15: b - (max (pp,((b + a) / 2))) <= b - pp by XREAL_1:13; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; b - P < b - (max (pp,((b + a) / 2))) by A12, XREAL_1:10; then b - P < r by A15, XXREAL_0:2; then dist (a9,P) < r by A13, Th14; then A16: P in Ball (a9,r) by METRIC_1:11; Q in IRRAT by Th17; then Q in A by A2, A14, XBOOLE_0:def_4; hence Ball (a9,r) meets A by A16, XBOOLE_0:3; ::_thesis: verum end; hence b in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; hence b in Cl A ; ::_thesis: verum end; theorem Th29: :: BORSUK_5:29 for a, b, c being real number holds ( c in RAT (a,b) iff ( c is rational & a < c & c < b ) ) proof let a, b, c be real number ; ::_thesis: ( c in RAT (a,b) iff ( c is rational & a < c & c < b ) ) hereby ::_thesis: ( c is rational & a < c & c < b implies c in RAT (a,b) ) assume A1: c in RAT (a,b) ; ::_thesis: ( c is rational & a < c & c < b ) then c in ].a,b.[ by XBOOLE_0:def_4; hence ( c is rational & a < c & c < b ) by A1, XXREAL_1:4; ::_thesis: verum end; assume that A2: c is rational and A3: a < c and A4: c < b ; ::_thesis: c in RAT (a,b) A5: c in RAT by A2, RAT_1:def_2; c in ].a,b.[ by A3, A4, XXREAL_1:4; hence c in RAT (a,b) by A5, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th30: :: BORSUK_5:30 for a, b, c being real number holds ( c in IRRAT (a,b) iff ( c is irrational & a < c & c < b ) ) proof let a, b, c be real number ; ::_thesis: ( c in IRRAT (a,b) iff ( c is irrational & a < c & c < b ) ) hereby ::_thesis: ( c is irrational & a < c & c < b implies c in IRRAT (a,b) ) assume A1: c in IRRAT (a,b) ; ::_thesis: ( c is irrational & a < c & c < b ) then A2: c in ].a,b.[ by XBOOLE_0:def_4; c in IRRAT by A1, XBOOLE_0:def_4; hence ( c is irrational & a < c & c < b ) by A2, Th17, XXREAL_1:4; ::_thesis: verum end; assume that A3: c is irrational and A4: a < c and A5: c < b ; ::_thesis: c in IRRAT (a,b) A6: c in ].a,b.[ by A4, A5, XXREAL_1:4; c in IRRAT by A3, Th17; hence c in IRRAT (a,b) by A6, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th31: :: BORSUK_5:31 for A being Subset of R^1 for a, b being real number st a < b & A = RAT (a,b) holds Cl A = [.a,b.] proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = RAT (a,b) holds Cl A = [.a,b.] let a, b be real number ; ::_thesis: ( a < b & A = RAT (a,b) implies Cl A = [.a,b.] ) assume that A1: a < b and A2: A = RAT (a,b) ; ::_thesis: Cl A = [.a,b.] reconsider ab = ].a,b.[, RT = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17; reconsider RR = RAT /\ ].a,b.[ as Subset of R^1 by TOPMETR:17; A3: the carrier of R^1 /\ (Cl ab) = Cl ab by XBOOLE_1:28; A4: Cl RR c= (Cl RT) /\ (Cl ab) by PRE_TOPC:21; thus Cl A c= [.a,b.] :: according to XBOOLE_0:def_10 ::_thesis: [.a,b.] c= Cl A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in [.a,b.] ) assume x in Cl A ; ::_thesis: x in [.a,b.] then x in (Cl RT) /\ (Cl ab) by A2, A4; then x in the carrier of R^1 /\ (Cl ab) by Th15; hence x in [.a,b.] by A1, A3, Th16; ::_thesis: verum end; thus [.a,b.] c= Cl A ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.] or x in Cl A ) assume A5: x in [.a,b.] ; ::_thesis: x in Cl A then reconsider p = x as Element of RealSpace by METRIC_1:def_13; A6: a <= p by A5, XXREAL_1:1; A7: p <= b by A5, XXREAL_1:1; percases ( p < b or p = b ) by A7, XXREAL_0:1; supposeA8: p < b ; ::_thesis: x in Cl A now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_ Ball_(p,r)_meets_A let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A ) reconsider pp = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; set pr = min (pp,((p + b) / 2)); A9: min (pp,((p + b) / 2)) <= (p + b) / 2 by XXREAL_0:17; assume A10: r > 0 ; ::_thesis: Ball (p,r) meets A p < min (pp,((p + b) / 2)) proof percases ( min (pp,((p + b) / 2)) = pp or min (pp,((p + b) / 2)) = (p + b) / 2 ) by XXREAL_0:15; suppose min (pp,((p + b) / 2)) = pp ; ::_thesis: p < min (pp,((p + b) / 2)) hence p < min (pp,((p + b) / 2)) by A10, XREAL_1:29; ::_thesis: verum end; suppose min (pp,((p + b) / 2)) = (p + b) / 2 ; ::_thesis: p < min (pp,((p + b) / 2)) hence p < min (pp,((p + b) / 2)) by A8, XREAL_1:226; ::_thesis: verum end; end; end; then consider Q being rational number such that A11: p < Q and A12: Q < min (pp,((p + b) / 2)) by RAT_1:7; (p + b) / 2 < b by A8, XREAL_1:226; then min (pp,((p + b) / 2)) < b by A9, XXREAL_0:2; then A13: Q < b by A12, XXREAL_0:2; min (pp,((p + b) / 2)) <= pp by XXREAL_0:17; then A14: (min (pp,((p + b) / 2))) - p <= pp - p by XREAL_1:9; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; P - p < (min (pp,((p + b) / 2))) - p by A12, XREAL_1:9; then P - p < r by A14, XXREAL_0:2; then dist (p,P) < r by A11, Th14; then A15: P in Ball (p,r) by METRIC_1:11; a < Q by A6, A11, XXREAL_0:2; then A16: Q in ].a,b.[ by A13, XXREAL_1:4; Q in RAT by RAT_1:def_2; then Q in A by A2, A16, XBOOLE_0:def_4; hence Ball (p,r) meets A by A15, XBOOLE_0:3; ::_thesis: verum end; hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; suppose p = b ; ::_thesis: x in Cl A hence x in Cl A by A1, A2, Lm2; ::_thesis: verum end; end; end; end; theorem Th32: :: BORSUK_5:32 for A being Subset of R^1 for a, b being real number st a < b & A = IRRAT (a,b) holds Cl A = [.a,b.] proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = IRRAT (a,b) holds Cl A = [.a,b.] let a, b be real number ; ::_thesis: ( a < b & A = IRRAT (a,b) implies Cl A = [.a,b.] ) assume that A1: a < b and A2: A = IRRAT (a,b) ; ::_thesis: Cl A = [.a,b.] reconsider ab = ].a,b.[, RT = IRRAT as Subset of R^1 by TOPMETR:17; reconsider RR = IRRAT /\ ].a,b.[ as Subset of R^1 by TOPMETR:17; A3: the carrier of R^1 /\ (Cl ab) = Cl ab by XBOOLE_1:28; A4: Cl RR c= (Cl RT) /\ (Cl ab) by PRE_TOPC:21; thus Cl A c= [.a,b.] :: according to XBOOLE_0:def_10 ::_thesis: [.a,b.] c= Cl A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in [.a,b.] ) assume x in Cl A ; ::_thesis: x in [.a,b.] then x in (Cl RT) /\ (Cl ab) by A2, A4; then x in the carrier of R^1 /\ (Cl ab) by Th28; hence x in [.a,b.] by A1, A3, Th16; ::_thesis: verum end; thus [.a,b.] c= Cl A ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.] or x in Cl A ) assume A5: x in [.a,b.] ; ::_thesis: x in Cl A then reconsider p = x as Element of RealSpace by METRIC_1:def_13; A6: a <= p by A5, XXREAL_1:1; A7: p <= b by A5, XXREAL_1:1; percases ( p < b or p = b ) by A7, XXREAL_0:1; supposeA8: p < b ; ::_thesis: x in Cl A now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_ Ball_(p,r)_meets_A let r be real number ; ::_thesis: ( r > 0 implies Ball (p,r) meets A ) reconsider pp = p + r as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; set pr = min (pp,((p + b) / 2)); A9: min (pp,((p + b) / 2)) <= (p + b) / 2 by XXREAL_0:17; assume A10: r > 0 ; ::_thesis: Ball (p,r) meets A p < min (pp,((p + b) / 2)) proof percases ( min (pp,((p + b) / 2)) = pp or min (pp,((p + b) / 2)) = (p + b) / 2 ) by XXREAL_0:15; suppose min (pp,((p + b) / 2)) = pp ; ::_thesis: p < min (pp,((p + b) / 2)) hence p < min (pp,((p + b) / 2)) by A10, XREAL_1:29; ::_thesis: verum end; suppose min (pp,((p + b) / 2)) = (p + b) / 2 ; ::_thesis: p < min (pp,((p + b) / 2)) hence p < min (pp,((p + b) / 2)) by A8, XREAL_1:226; ::_thesis: verum end; end; end; then consider Q being real irrational number such that A11: p < Q and A12: Q < min (pp,((p + b) / 2)) by Th27; (p + b) / 2 < b by A8, XREAL_1:226; then min (pp,((p + b) / 2)) < b by A9, XXREAL_0:2; then A13: Q < b by A12, XXREAL_0:2; min (pp,((p + b) / 2)) <= pp by XXREAL_0:17; then A14: (min (pp,((p + b) / 2))) - p <= pp - p by XREAL_1:9; reconsider P = Q as Element of RealSpace by METRIC_1:def_13, XREAL_0:def_1; P - p < (min (pp,((p + b) / 2))) - p by A12, XREAL_1:9; then P - p < r by A14, XXREAL_0:2; then dist (p,P) < r by A11, Th14; then A15: P in Ball (p,r) by METRIC_1:11; a < Q by A6, A11, XXREAL_0:2; then A16: Q in ].a,b.[ by A13, XXREAL_1:4; Q in IRRAT by Th17; then Q in A by A2, A16, XBOOLE_0:def_4; hence Ball (p,r) meets A by A15, XBOOLE_0:3; ::_thesis: verum end; hence x in Cl A by GOBOARD6:92, TOPMETR:def_6; ::_thesis: verum end; suppose p = b ; ::_thesis: x in Cl A hence x in Cl A by A1, A2, Lm3; ::_thesis: verum end; end; end; end; theorem Th33: :: BORSUK_5:33 for T being connected TopSpace for A being open closed Subset of T holds ( A = {} or A = [#] T ) proof let T be connected TopSpace; ::_thesis: for A being open closed Subset of T holds ( A = {} or A = [#] T ) let A be open closed Subset of T; ::_thesis: ( A = {} or A = [#] T ) assume that A1: A <> {} and A2: A <> [#] T ; ::_thesis: contradiction A3: A ` <> {} by A2, PRE_TOPC:4; A misses A ` by SUBSET_1:24; then A4: A,A ` are_separated by CONNSP_1:2; A5: [#] T = A \/ (A `) by PRE_TOPC:2; A <> {} T by A1; then not [#] T is connected by A5, A4, A3, CONNSP_1:15; hence contradiction by CONNSP_1:27; ::_thesis: verum end; theorem Th34: :: BORSUK_5:34 for A being Subset of R^1 st A is closed & A is open & not A = {} holds A = REAL proof let A be Subset of R^1; ::_thesis: ( A is closed & A is open & not A = {} implies A = REAL ) assume ( A is closed & A is open ) ; ::_thesis: ( A = {} or A = REAL ) then reconsider A = A as open closed Subset of R^1 ; ( A = {} or A = [#] R^1 ) by Th33; hence ( A = {} or A = REAL ) by TOPMETR:17; ::_thesis: verum end; begin theorem Th35: :: BORSUK_5:35 for A being Subset of R^1 for a, b being real number st A = [.a,b.[ & a <> b holds Cl A = [.a,b.] proof let A be Subset of R^1; ::_thesis: for a, b being real number st A = [.a,b.[ & a <> b holds Cl A = [.a,b.] let a, b be real number ; ::_thesis: ( A = [.a,b.[ & a <> b implies Cl A = [.a,b.] ) assume that A1: A = [.a,b.[ and A2: a <> b ; ::_thesis: Cl A = [.a,b.] Cl [.a,b.[ = [.a,b.] by A2, BORSUK_4:12; hence Cl A = [.a,b.] by A1, JORDAN5A:24; ::_thesis: verum end; theorem Th36: :: BORSUK_5:36 for A being Subset of R^1 for a, b being real number st A = ].a,b.] & a <> b holds Cl A = [.a,b.] proof let A be Subset of R^1; ::_thesis: for a, b being real number st A = ].a,b.] & a <> b holds Cl A = [.a,b.] let a, b be real number ; ::_thesis: ( A = ].a,b.] & a <> b implies Cl A = [.a,b.] ) assume that A1: A = ].a,b.] and A2: a <> b ; ::_thesis: Cl A = [.a,b.] Cl ].a,b.] = [.a,b.] by A2, BORSUK_4:11; hence Cl A = [.a,b.] by A1, JORDAN5A:24; ::_thesis: verum end; theorem :: BORSUK_5:37 for A being Subset of R^1 for a, b, c being real number st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds Cl A = [.a,c.] proof let A be Subset of R^1; ::_thesis: for a, b, c being real number st A = [.a,b.[ \/ ].b,c.] & a < b & b < c holds Cl A = [.a,c.] let a, b, c be real number ; ::_thesis: ( A = [.a,b.[ \/ ].b,c.] & a < b & b < c implies Cl A = [.a,c.] ) assume that A1: A = [.a,b.[ \/ ].b,c.] and A2: a < b and A3: b < c ; ::_thesis: Cl A = [.a,c.] reconsider B = [.a,b.[, C = ].b,c.] as Subset of R^1 by TOPMETR:17; Cl A = (Cl B) \/ (Cl C) by A1, PRE_TOPC:20 .= [.a,b.] \/ (Cl C) by A2, Th35 .= [.a,b.] \/ [.b,c.] by A3, Th36 .= [.a,c.] by A2, A3, XXREAL_1:174 ; hence Cl A = [.a,c.] ; ::_thesis: verum end; theorem Th38: :: BORSUK_5:38 for A being Subset of R^1 for a being real number st A = {a} holds Cl A = {a} proof let A be Subset of R^1; ::_thesis: for a being real number st A = {a} holds Cl A = {a} let a be real number ; ::_thesis: ( A = {a} implies Cl A = {a} ) A1: a is Point of R^1 by TOPMETR:17, XREAL_0:def_1; assume A = {a} ; ::_thesis: Cl A = {a} hence Cl A = {a} by A1, YELLOW_8:26; ::_thesis: verum end; theorem Th39: :: BORSUK_5:39 for A being Subset of REAL for B being Subset of R^1 st A = B holds ( A is open iff B is open ) proof let A be Subset of REAL; ::_thesis: for B being Subset of R^1 st A = B holds ( A is open iff B is open ) let B be Subset of R^1; ::_thesis: ( A = B implies ( A is open iff B is open ) ) assume A1: A = B ; ::_thesis: ( A is open iff B is open ) hereby ::_thesis: ( B is open implies A is open ) assume A is open ; ::_thesis: B is open then A in Family_open_set RealSpace by JORDAN5A:5; then A in the topology of (TopSpaceMetr RealSpace) by TOPMETR:12; hence B is open by A1, PRE_TOPC:def_2, TOPMETR:def_6; ::_thesis: verum end; assume B is open ; ::_thesis: A is open then B in the topology of R^1 by PRE_TOPC:def_2; then A in Family_open_set RealSpace by A1, TOPMETR:12, TOPMETR:def_6; hence A is open by JORDAN5A:5; ::_thesis: verum end; Lm4: for a being real number holds ].-infty,a.] is closed proof let a be real number ; ::_thesis: ].-infty,a.] is closed ].-infty,a.] = left_closed_halfline a ; hence ].-infty,a.] is closed ; ::_thesis: verum end; Lm5: for a being real number holds [.a,+infty.[ is closed proof let a be real number ; ::_thesis: [.a,+infty.[ is closed [.a,+infty.[ = right_closed_halfline a ; hence [.a,+infty.[ is closed ; ::_thesis: verum end; registration let A, B be open Subset of REAL; reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17; clusterA /\ B -> open for Subset of REAL; coherence for b1 being Subset of REAL st b1 = A /\ B holds b1 is open proof A1: B1 is open by Th39; A1 is open by Th39; then A1 /\ B1 is open by A1; hence for b1 being Subset of REAL st b1 = A /\ B holds b1 is open by Th39; ::_thesis: verum end; clusterA \/ B -> open for Subset of REAL; coherence for b1 being Subset of REAL st b1 = A \/ B holds b1 is open proof A2: B1 is open by Th39; A1 is open by Th39; then A1 \/ B1 is open by A2; hence for b1 being Subset of REAL st b1 = A \/ B holds b1 is open by Th39; ::_thesis: verum end; end; Lm6: for a, b being ext-real number holds ].a,b.[ is open proof let a, b be ext-real number ; ::_thesis: ].a,b.[ is open set A = ].a,b.[; percases ( ( a in REAL & b in REAL ) or a = +infty or ( a = -infty & b in REAL ) or ( a in REAL & b = +infty ) or b = -infty or ( a = -infty & b = +infty ) ) by XXREAL_0:14; suppose ( a in REAL & b in REAL ) ; ::_thesis: ].a,b.[ is open then reconsider a = a, b = b as real number ; ].a,b.[ = ].-infty,b.[ /\ ].a,+infty.[ by XXREAL_1:269; hence ].a,b.[ is open ; ::_thesis: verum end; suppose a = +infty ; ::_thesis: ].a,b.[ is open then ].a,b.[ = {} by XXREAL_1:214; hence ].a,b.[ is open ; ::_thesis: verum end; supposethat A1: a = -infty and A2: b in REAL ; ::_thesis: ].a,b.[ is open reconsider b = b as real number by A2; ].a,b.[ = left_open_halfline b by A1; hence ].a,b.[ is open ; ::_thesis: verum end; supposethat A3: a in REAL and A4: b = +infty ; ::_thesis: ].a,b.[ is open reconsider a = a as real number by A3; ].a,b.[ = right_open_halfline a by A4; hence ].a,b.[ is open ; ::_thesis: verum end; suppose b = -infty ; ::_thesis: ].a,b.[ is open then ].a,b.[ = {} by XXREAL_1:210; hence ].a,b.[ is open ; ::_thesis: verum end; suppose ( a = -infty & b = +infty ) ; ::_thesis: ].a,b.[ is open then ].a,b.[ = [#] REAL by XXREAL_1:224; hence ].a,b.[ is open ; ::_thesis: verum end; end; end; theorem Th40: :: BORSUK_5:40 for A being Subset of R^1 for a, b being ext-real number st A = ].a,b.[ holds A is open proof let A be Subset of R^1; ::_thesis: for a, b being ext-real number st A = ].a,b.[ holds A is open let a, b be ext-real number ; ::_thesis: ( A = ].a,b.[ implies A is open ) ].a,b.[ is open by Lm6; hence ( A = ].a,b.[ implies A is open ) by Th39; ::_thesis: verum end; theorem Th41: :: BORSUK_5:41 for A being Subset of R^1 for a being real number st A = ].-infty,a.] holds A is closed proof let A be Subset of R^1; ::_thesis: for a being real number st A = ].-infty,a.] holds A is closed let a be real number ; ::_thesis: ( A = ].-infty,a.] implies A is closed ) assume A1: A = ].-infty,a.] ; ::_thesis: A is closed ].-infty,a.] is closed by Lm4; hence A is closed by A1, JORDAN5A:23; ::_thesis: verum end; theorem Th42: :: BORSUK_5:42 for A being Subset of R^1 for a being real number st A = [.a,+infty.[ holds A is closed proof let A be Subset of R^1; ::_thesis: for a being real number st A = [.a,+infty.[ holds A is closed let a be real number ; ::_thesis: ( A = [.a,+infty.[ implies A is closed ) assume A1: A = [.a,+infty.[ ; ::_thesis: A is closed [.a,+infty.[ is closed by Lm5; hence A is closed by A1, JORDAN5A:23; ::_thesis: verum end; theorem Th43: :: BORSUK_5:43 for a being real number holds [.a,+infty.[ = {a} \/ ].a,+infty.[ proof let a be real number ; ::_thesis: [.a,+infty.[ = {a} \/ ].a,+infty.[ thus [.a,+infty.[ c= {a} \/ ].a,+infty.[ :: according to XBOOLE_0:def_10 ::_thesis: {a} \/ ].a,+infty.[ c= [.a,+infty.[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,+infty.[ or x in {a} \/ ].a,+infty.[ ) assume A1: x in [.a,+infty.[ ; ::_thesis: x in {a} \/ ].a,+infty.[ then reconsider x = x as real number ; A2: x >= a by A1, XXREAL_1:236; percases ( x = a or x > a ) by A2, XXREAL_0:1; suppose x = a ; ::_thesis: x in {a} \/ ].a,+infty.[ then x in {a} by TARSKI:def_1; hence x in {a} \/ ].a,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; suppose x > a ; ::_thesis: x in {a} \/ ].a,+infty.[ then x in ].a,+infty.[ by XXREAL_1:235; hence x in {a} \/ ].a,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} \/ ].a,+infty.[ or x in [.a,+infty.[ ) assume A3: x in {a} \/ ].a,+infty.[ ; ::_thesis: x in [.a,+infty.[ then reconsider x = x as real number ; ( x in {a} or x in ].a,+infty.[ ) by A3, XBOOLE_0:def_3; then ( x = a or x > a ) by TARSKI:def_1, XXREAL_1:235; hence x in [.a,+infty.[ by XXREAL_1:236; ::_thesis: verum end; theorem Th44: :: BORSUK_5:44 for a being real number holds ].-infty,a.] = {a} \/ ].-infty,a.[ proof let a be real number ; ::_thesis: ].-infty,a.] = {a} \/ ].-infty,a.[ thus ].-infty,a.] c= {a} \/ ].-infty,a.[ :: according to XBOOLE_0:def_10 ::_thesis: {a} \/ ].-infty,a.[ c= ].-infty,a.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,a.] or x in {a} \/ ].-infty,a.[ ) assume A1: x in ].-infty,a.] ; ::_thesis: x in {a} \/ ].-infty,a.[ then reconsider x = x as real number ; A2: x <= a by A1, XXREAL_1:234; percases ( x = a or x < a ) by A2, XXREAL_0:1; suppose x = a ; ::_thesis: x in {a} \/ ].-infty,a.[ then x in {a} by TARSKI:def_1; hence x in {a} \/ ].-infty,a.[ by XBOOLE_0:def_3; ::_thesis: verum end; suppose x < a ; ::_thesis: x in {a} \/ ].-infty,a.[ then x in ].-infty,a.[ by XXREAL_1:233; hence x in {a} \/ ].-infty,a.[ by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} \/ ].-infty,a.[ or x in ].-infty,a.] ) assume A3: x in {a} \/ ].-infty,a.[ ; ::_thesis: x in ].-infty,a.] then reconsider x = x as real number ; ( x in {a} or x in ].-infty,a.[ ) by A3, XBOOLE_0:def_3; then ( x = a or x < a ) by TARSKI:def_1, XXREAL_1:233; hence x in ].-infty,a.] by XXREAL_1:234; ::_thesis: verum end; registration let a be real number ; clusterK451(a,+infty) -> non empty ; coherence not ].a,+infty.[ is empty proof a < a + 1 by XREAL_1:29; hence not ].a,+infty.[ is empty by XXREAL_1:235; ::_thesis: verum end; clusterK450(-infty,a) -> non empty ; coherence not ].-infty,a.] is empty by XXREAL_1:234; clusterK451(-infty,a) -> non empty ; coherence not ].-infty,a.[ is empty proof a - 1 < a by XREAL_1:146; hence not ].-infty,a.[ is empty by XXREAL_1:233; ::_thesis: verum end; clusterK449(a,+infty) -> non empty ; coherence not [.a,+infty.[ is empty by XXREAL_1:236; end; theorem Th45: :: BORSUK_5:45 for a being real number holds ].a,+infty.[ <> REAL proof let a be real number ; ::_thesis: ].a,+infty.[ <> REAL a in REAL by XREAL_0:def_1; hence ].a,+infty.[ <> REAL by XXREAL_1:235; ::_thesis: verum end; theorem :: BORSUK_5:46 for a being real number holds [.a,+infty.[ <> REAL proof let a be real number ; ::_thesis: [.a,+infty.[ <> REAL A1: a - 1 < a by XREAL_1:146; a - 1 in REAL by XREAL_0:def_1; hence [.a,+infty.[ <> REAL by A1, XXREAL_1:236; ::_thesis: verum end; theorem :: BORSUK_5:47 for a being real number holds ].-infty,a.] <> REAL proof let a be real number ; ::_thesis: ].-infty,a.] <> REAL A1: a + 1 > a by XREAL_1:29; a + 1 in REAL by XREAL_0:def_1; hence ].-infty,a.] <> REAL by A1, XXREAL_1:234; ::_thesis: verum end; theorem Th48: :: BORSUK_5:48 for a being real number holds ].-infty,a.[ <> REAL proof let a be real number ; ::_thesis: ].-infty,a.[ <> REAL A1: a + 1 > a by XREAL_1:29; a + 1 in REAL by XREAL_0:def_1; hence ].-infty,a.[ <> REAL by A1, XXREAL_1:233; ::_thesis: verum end; theorem Th49: :: BORSUK_5:49 for A being Subset of R^1 for a being real number st A = ].a,+infty.[ holds Cl A = [.a,+infty.[ proof let A be Subset of R^1; ::_thesis: for a being real number st A = ].a,+infty.[ holds Cl A = [.a,+infty.[ let a be real number ; ::_thesis: ( A = ].a,+infty.[ implies Cl A = [.a,+infty.[ ) reconsider A9 = A as Subset of R^1 ; reconsider C = [.a,+infty.[ as Subset of R^1 by TOPMETR:17; assume A1: A = ].a,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[ then A2: A9 is open by Th40; C is closed by Th42; then A3: Cl A9 c= C by A1, TOPS_1:5, XXREAL_1:45; A4: C = A9 \/ {a} by A1, Th43; percases ( Cl A9 = C or Cl A9 = A9 ) by A4, A3, ZFMISC_1:138, PRE_TOPC:18; suppose Cl A9 = C ; ::_thesis: Cl A = [.a,+infty.[ hence Cl A = [.a,+infty.[ ; ::_thesis: verum end; suppose Cl A9 = A9 ; ::_thesis: Cl A = [.a,+infty.[ hence Cl A = [.a,+infty.[ by A1, A2, Th34, Th45; ::_thesis: verum end; end; end; theorem :: BORSUK_5:50 for a being real number holds Cl ].a,+infty.[ = [.a,+infty.[ proof let a be real number ; ::_thesis: Cl ].a,+infty.[ = [.a,+infty.[ reconsider A = ].a,+infty.[ as Subset of R^1 by TOPMETR:17; Cl A = [.a,+infty.[ by Th49; hence Cl ].a,+infty.[ = [.a,+infty.[ by JORDAN5A:24; ::_thesis: verum end; theorem Th51: :: BORSUK_5:51 for A being Subset of R^1 for a being real number st A = ].-infty,a.[ holds Cl A = ].-infty,a.] proof let A be Subset of R^1; ::_thesis: for a being real number st A = ].-infty,a.[ holds Cl A = ].-infty,a.] let a be real number ; ::_thesis: ( A = ].-infty,a.[ implies Cl A = ].-infty,a.] ) reconsider A9 = A as Subset of R^1 ; reconsider C = ].-infty,a.] as Subset of R^1 by TOPMETR:17; assume A1: A = ].-infty,a.[ ; ::_thesis: Cl A = ].-infty,a.] then A2: A9 is open by Th40; C is closed by Th41; then A3: Cl A9 c= C by A1, TOPS_1:5, XXREAL_1:41; A4: C = A9 \/ {a} by A1, Th44; percases ( Cl A9 = C or Cl A9 = A9 ) by A4, A3, ZFMISC_1:138, PRE_TOPC:18; suppose Cl A9 = C ; ::_thesis: Cl A = ].-infty,a.] hence Cl A = ].-infty,a.] ; ::_thesis: verum end; suppose Cl A9 = A9 ; ::_thesis: Cl A = ].-infty,a.] hence Cl A = ].-infty,a.] by A1, A2, Th34, Th48; ::_thesis: verum end; end; end; theorem :: BORSUK_5:52 for a being real number holds Cl ].-infty,a.[ = ].-infty,a.] proof let a be real number ; ::_thesis: Cl ].-infty,a.[ = ].-infty,a.] reconsider A = ].-infty,a.[ as Subset of R^1 by TOPMETR:17; Cl A = ].-infty,a.] by Th51; hence Cl ].-infty,a.[ = ].-infty,a.] by JORDAN5A:24; ::_thesis: verum end; theorem Th53: :: BORSUK_5:53 for A, B being Subset of R^1 for b being real number st A = ].-infty,b.[ & B = ].b,+infty.[ holds A,B are_separated proof let A, B be Subset of R^1; ::_thesis: for b being real number st A = ].-infty,b.[ & B = ].b,+infty.[ holds A,B are_separated let b be real number ; ::_thesis: ( A = ].-infty,b.[ & B = ].b,+infty.[ implies A,B are_separated ) assume that A1: A = ].-infty,b.[ and A2: B = ].b,+infty.[ ; ::_thesis: A,B are_separated Cl B = [.b,+infty.[ by A2, Th49; then A3: Cl B misses A by A1, XXREAL_1:94; Cl A = ].-infty,b.] by A1, Th51; then Cl A misses B by A2, XXREAL_1:91; hence A,B are_separated by A3, CONNSP_1:def_1; ::_thesis: verum end; theorem :: BORSUK_5:54 for A being Subset of R^1 for a, b being real number st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds Cl A = [.a,+infty.[ proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = [.a,b.[ \/ ].b,+infty.[ holds Cl A = [.a,+infty.[ let a, b be real number ; ::_thesis: ( a < b & A = [.a,b.[ \/ ].b,+infty.[ implies Cl A = [.a,+infty.[ ) assume that A1: a < b and A2: A = [.a,b.[ \/ ].b,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[ reconsider B = [.a,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17; A3: Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20; A4: Cl C = [.b,+infty.[ by Th49; Cl B = [.a,b.] by A1, Th35; hence Cl A = [.a,+infty.[ by A1, A4, A3, Th11; ::_thesis: verum end; theorem Th55: :: BORSUK_5:55 for A being Subset of R^1 for a, b being real number st a < b & A = ].a,b.[ \/ ].b,+infty.[ holds Cl A = [.a,+infty.[ proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = ].a,b.[ \/ ].b,+infty.[ holds Cl A = [.a,+infty.[ let a, b be real number ; ::_thesis: ( a < b & A = ].a,b.[ \/ ].b,+infty.[ implies Cl A = [.a,+infty.[ ) assume that A1: a < b and A2: A = ].a,b.[ \/ ].b,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[ reconsider B = ].a,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17; A3: Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20; A4: Cl C = [.b,+infty.[ by Th49; Cl B = [.a,b.] by A1, Th16; hence Cl A = [.a,+infty.[ by A1, A3, A4, Th11; ::_thesis: verum end; theorem :: BORSUK_5:56 for A being Subset of R^1 for a, b, c being real number st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds Cl A = [.a,+infty.[ proof let A be Subset of R^1; ::_thesis: for a, b, c being real number st a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ holds Cl A = [.a,+infty.[ let a, b, c be real number ; ::_thesis: ( a < b & b < c & A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ implies Cl A = [.a,+infty.[ ) assume that A1: a < b and A2: b < c ; ::_thesis: ( not A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ or Cl A = [.a,+infty.[ ) reconsider B = RAT (a,b) as Subset of R^1 by TOPMETR:17; reconsider C = ].b,c.[ \/ ].c,+infty.[ as Subset of R^1 by TOPMETR:17; assume A = ((RAT (a,b)) \/ ].b,c.[) \/ ].c,+infty.[ ; ::_thesis: Cl A = [.a,+infty.[ then A = (RAT (a,b)) \/ C by XBOOLE_1:4; then Cl A = (Cl B) \/ (Cl C) by PRE_TOPC:20; then Cl A = (Cl B) \/ [.b,+infty.[ by A2, Th55; then Cl A = [.a,b.] \/ [.b,+infty.[ by A1, Th31; hence Cl A = [.a,+infty.[ by A1, Th11; ::_thesis: verum end; theorem Th57: :: BORSUK_5:57 for a, b being real number holds IRRAT (a,b) misses RAT (a,b) proof let a, b be real number ; ::_thesis: IRRAT (a,b) misses RAT (a,b) assume IRRAT (a,b) meets RAT (a,b) ; ::_thesis: contradiction then consider x being set such that A1: x in IRRAT (a,b) and A2: x in RAT (a,b) by XBOOLE_0:3; thus contradiction by A1, A2, Th30; ::_thesis: verum end; theorem Th58: :: BORSUK_5:58 for a, b being real number holds REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ proof let a, b be real number ; ::_thesis: REAL \ (RAT (a,b)) = (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ thus REAL \ (RAT (a,b)) c= (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ :: according to XBOOLE_0:def_10 ::_thesis: (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ c= REAL \ (RAT (a,b)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL \ (RAT (a,b)) or x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ ) assume A1: x in REAL \ (RAT (a,b)) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ then A2: not x in RAT (a,b) by XBOOLE_0:def_5; reconsider x = x as real number by A1; percases ( ( x <= a & x < b ) or ( x <= a & x >= b ) or ( x > a & x < b ) or ( x > a & x >= b ) ) ; suppose ( x <= a & x < b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ then x in ].-infty,a.] by XXREAL_1:234; then x in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3; hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x <= a & x >= b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ then x in ].-infty,a.] by XXREAL_1:234; then x in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3; hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; supposeA3: ( x > a & x < b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ x in IRRAT (a,b) proof percases ( x is rational or x is irrational ) ; suppose x is rational ; ::_thesis: x in IRRAT (a,b) hence x in IRRAT (a,b) by A2, A3, Th29; ::_thesis: verum end; suppose x is irrational ; ::_thesis: x in IRRAT (a,b) hence x in IRRAT (a,b) by A3, Th30; ::_thesis: verum end; end; end; then x in ].-infty,a.] \/ (IRRAT (a,b)) by XBOOLE_0:def_3; hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; suppose ( x > a & x >= b ) ; ::_thesis: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ then x in [.b,+infty.[ by XXREAL_1:236; hence x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ or x in REAL \ (RAT (a,b)) ) assume A4: x in (].-infty,a.] \/ (IRRAT (a,b))) \/ [.b,+infty.[ ; ::_thesis: x in REAL \ (RAT (a,b)) then reconsider x = x as real number ; A5: ( x in ].-infty,a.] \/ (IRRAT (a,b)) or x in [.b,+infty.[ ) by A4, XBOOLE_0:def_3; percases ( x in ].-infty,a.] or x in IRRAT (a,b) or x in [.b,+infty.[ ) by A5, XBOOLE_0:def_3; suppose x in ].-infty,a.] ; ::_thesis: x in REAL \ (RAT (a,b)) then x <= a by XXREAL_1:234; then A6: not x in RAT (a,b) by Th29; x in REAL by XREAL_0:def_1; hence x in REAL \ (RAT (a,b)) by A6, XBOOLE_0:def_5; ::_thesis: verum end; supposeA7: x in IRRAT (a,b) ; ::_thesis: x in REAL \ (RAT (a,b)) IRRAT (a,b) misses RAT (a,b) by Th57; then A8: not x in RAT (a,b) by A7, XBOOLE_0:3; x in REAL by XREAL_0:def_1; hence x in REAL \ (RAT (a,b)) by A8, XBOOLE_0:def_5; ::_thesis: verum end; suppose x in [.b,+infty.[ ; ::_thesis: x in REAL \ (RAT (a,b)) then x >= b by XXREAL_1:236; then A9: not x in RAT (a,b) by Th29; x in REAL by XREAL_0:def_1; hence x in REAL \ (RAT (a,b)) by A9, XBOOLE_0:def_5; ::_thesis: verum end; end; end; theorem Th59: :: BORSUK_5:59 for a, b being real number st a < b holds [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b} proof let a, b be real number ; ::_thesis: ( a < b implies [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b} ) A1: not b in ].a,b.[ \/ ].b,+infty.[ by XXREAL_1:205; assume A2: a < b ; ::_thesis: [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b} then A3: not a in ].a,b.[ \/ ].b,+infty.[ by XXREAL_1:223; [.a,+infty.[ = [.a,b.] \/ [.b,+infty.[ by A2, Th11 .= ({a,b} \/ ].a,b.[) \/ [.b,+infty.[ by A2, XXREAL_1:128 .= ({a,b} \/ ].a,b.[) \/ ({b} \/ ].b,+infty.[) by Th43 .= (({a,b} \/ ].a,b.[) \/ {b}) \/ ].b,+infty.[ by XBOOLE_1:4 .= (({a,b} \/ {b}) \/ ].a,b.[) \/ ].b,+infty.[ by XBOOLE_1:4 .= ({a,b} \/ ].a,b.[) \/ ].b,+infty.[ by ZFMISC_1:9 .= {a,b} \/ (].a,b.[ \/ ].b,+infty.[) by XBOOLE_1:4 ; then [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a,b} by A3, A1, XBOOLE_1:88, ZFMISC_1:51; hence [.a,+infty.[ \ (].a,b.[ \/ ].b,+infty.[) = {a} \/ {b} by ENUMSET1:1; ::_thesis: verum end; theorem :: BORSUK_5:60 for A being Subset of R^1 st A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ holds A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} proof A1: ].-infty,2.] \/ (IRRAT (2,4)) c= ].-infty,4.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,2.] \/ (IRRAT (2,4)) or x in ].-infty,4.] ) assume A2: x in ].-infty,2.] \/ (IRRAT (2,4)) ; ::_thesis: x in ].-infty,4.] then reconsider x = x as real number ; percases ( x in ].-infty,2.] or x in IRRAT (2,4) ) by A2, XBOOLE_0:def_3; suppose x in ].-infty,2.] ; ::_thesis: x in ].-infty,4.] then x <= 2 by XXREAL_1:234; then x <= 4 by XXREAL_0:2; hence x in ].-infty,4.] by XXREAL_1:234; ::_thesis: verum end; suppose x in IRRAT (2,4) ; ::_thesis: x in ].-infty,4.] then x < 4 by Th30; hence x in ].-infty,4.] by XXREAL_1:234; ::_thesis: verum end; end; end; let A be Subset of R^1; ::_thesis: ( A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ implies A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} ) A3: ].4,5.[ \/ ].5,+infty.[ c= ].4,+infty.[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].4,5.[ \/ ].5,+infty.[ or x in ].4,+infty.[ ) assume A4: x in ].4,5.[ \/ ].5,+infty.[ ; ::_thesis: x in ].4,+infty.[ then reconsider x = x as real number ; percases ( x in ].4,5.[ or x in ].5,+infty.[ ) by A4, XBOOLE_0:def_3; suppose x in ].4,5.[ ; ::_thesis: x in ].4,+infty.[ then x > 4 by XXREAL_1:4; hence x in ].4,+infty.[ by XXREAL_1:235; ::_thesis: verum end; suppose x in ].5,+infty.[ ; ::_thesis: x in ].4,+infty.[ then x > 5 by XXREAL_1:235; then x > 4 by XXREAL_0:2; hence x in ].4,+infty.[ by XXREAL_1:235; ::_thesis: verum end; end; end; assume A = ((RAT (2,4)) \/ ].4,5.[) \/ ].5,+infty.[ ; ::_thesis: A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} then A5: A ` = REAL \ ((RAT (2,4)) \/ (].4,5.[ \/ ].5,+infty.[)) by TOPMETR:17, XBOOLE_1:4 .= (REAL \ (RAT (2,4))) \ (].4,5.[ \/ ].5,+infty.[) by XBOOLE_1:41 .= ((].-infty,2.] \/ (IRRAT (2,4))) \/ [.4,+infty.[) \ (].4,5.[ \/ ].5,+infty.[) by Th58 ; ].-infty,4.] misses ].4,+infty.[ by XXREAL_1:91; then A ` = ([.4,+infty.[ \ (].4,5.[ \/ ].5,+infty.[)) \/ (].-infty,2.] \/ (IRRAT (2,4))) by A5, A1, A3, XBOOLE_1:64, XBOOLE_1:87 .= (].-infty,2.] \/ (IRRAT (2,4))) \/ ({4} \/ {5}) by Th59 .= ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:4 ; hence A ` = ((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} ; ::_thesis: verum end; theorem :: BORSUK_5:61 for A being Subset of R^1 for a being real number st A = {a} holds A ` = ].-infty,a.[ \/ ].a,+infty.[ by TOPMETR:17, XXREAL_1:389; Lm7: ((IRRAT (2,4)) \/ {4}) \/ {5} c= ].1,+infty.[ proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((IRRAT (2,4)) \/ {4}) \/ {5} or x in ].1,+infty.[ ) assume A1: x in ((IRRAT (2,4)) \/ {4}) \/ {5} ; ::_thesis: x in ].1,+infty.[ then reconsider x = x as real number ; A2: ( x in (IRRAT (2,4)) \/ {4} or x in {5} ) by A1, XBOOLE_0:def_3; percases ( x in IRRAT (2,4) or x in {4} or x in {5} ) by A2, XBOOLE_0:def_3; suppose x in IRRAT (2,4) ; ::_thesis: x in ].1,+infty.[ then x > 2 by Th30; then x > 1 by XXREAL_0:2; hence x in ].1,+infty.[ by XXREAL_1:235; ::_thesis: verum end; suppose x in {4} ; ::_thesis: x in ].1,+infty.[ then x = 4 by TARSKI:def_1; hence x in ].1,+infty.[ by XXREAL_1:235; ::_thesis: verum end; suppose x in {5} ; ::_thesis: x in ].1,+infty.[ then x = 5 by TARSKI:def_1; hence x in ].1,+infty.[ by XXREAL_1:235; ::_thesis: verum end; end; end; Lm8: ].1,+infty.[ c= [.1,+infty.[ by XXREAL_1:45; Lm9: ].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ proof A1: ].-infty,1.[ c= ].-infty,2.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ].-infty,1.[ or x in ].-infty,2.] ) assume A2: x in ].-infty,1.[ ; ::_thesis: x in ].-infty,2.] then reconsider x = x as real number ; x < 1 by A2, XXREAL_1:233; then x < 2 by XXREAL_0:2; hence x in ].-infty,2.] by XXREAL_1:234; ::_thesis: verum end; [.1,+infty.[ misses ].-infty,1.[ by XXREAL_1:94; then A3: ((IRRAT (2,4)) \/ {4}) \/ {5} misses ].-infty,1.[ by Lm7, Lm8, XBOOLE_1:1, XBOOLE_1:63; ].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ /\ (].-infty,2.] \/ (((IRRAT (2,4)) \/ {4}) \/ {5})) by XBOOLE_1:113 .= ].-infty,1.[ /\ ].-infty,2.] by A3, XBOOLE_1:78 .= ].-infty,1.[ by A1, XBOOLE_1:28 ; hence ].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ ; ::_thesis: verum end; Lm10: ].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} proof ].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].1,+infty.[ /\ (].-infty,2.] \/ (((IRRAT (2,4)) \/ {4}) \/ {5})) by XBOOLE_1:113 .= (].1,+infty.[ /\ ].-infty,2.]) \/ (].1,+infty.[ /\ (((IRRAT (2,4)) \/ {4}) \/ {5})) by XBOOLE_1:23 .= (].1,+infty.[ /\ ].-infty,2.]) \/ (((IRRAT (2,4)) \/ {4}) \/ {5}) by Lm7, XBOOLE_1:28 .= ].1,2.] \/ (((IRRAT (2,4)) \/ {4}) \/ {5}) by XXREAL_1:270 .= ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:113 ; hence ].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5} ; ::_thesis: verum end; theorem :: BORSUK_5:62 (].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5} proof (].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[ \/ (].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5})) by Lm9, XBOOLE_1:23 .= ].-infty,1.[ \/ ((].1,2.] \/ (IRRAT (2,4))) \/ ({4} \/ {5})) by Lm10, XBOOLE_1:4 .= ((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ ({4} \/ {5}) by XBOOLE_1:113 ; hence (].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = (((].-infty,1.[ \/ ].1,2.]) \/ (IRRAT (2,4))) \/ {4}) \/ {5} by XBOOLE_1:4; ::_thesis: verum end; theorem :: BORSUK_5:63 for A being Subset of R^1 for a, b being real number st a <= b & A = {a} \/ [.b,+infty.[ holds A ` = ].-infty,a.[ \/ ].a,b.[ proof let A be Subset of R^1; ::_thesis: for a, b being real number st a <= b & A = {a} \/ [.b,+infty.[ holds A ` = ].-infty,a.[ \/ ].a,b.[ let a, b be real number ; ::_thesis: ( a <= b & A = {a} \/ [.b,+infty.[ implies A ` = ].-infty,a.[ \/ ].a,b.[ ) assume that A1: a <= b and A2: A = {a} \/ [.b,+infty.[ ; ::_thesis: A ` = ].-infty,a.[ \/ ].a,b.[ A ` = (REAL \ [.b,+infty.[) \ {a} by A2, TOPMETR:17, XBOOLE_1:41 .= ].-infty,b.[ \ {a} by XXREAL_1:224, XXREAL_1:294 ; hence A ` = ].-infty,a.[ \/ ].a,b.[ by A1, XXREAL_1:349; ::_thesis: verum end; theorem :: BORSUK_5:64 for A being Subset of R^1 for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.[ holds Cl A = ].-infty,b.] proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.[ holds Cl A = ].-infty,b.] let a, b be real number ; ::_thesis: ( a < b & A = ].-infty,a.[ \/ ].a,b.[ implies Cl A = ].-infty,b.] ) assume that A1: a < b and A2: A = ].-infty,a.[ \/ ].a,b.[ ; ::_thesis: Cl A = ].-infty,b.] reconsider B = ].-infty,a.[, C = ].a,b.[ as Subset of R^1 by TOPMETR:17; A3: Cl C = [.a,b.] by A1, Th16; Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20 .= ].-infty,a.] \/ [.a,b.] by A3, Th51 .= ].-infty,b.] by A1, Th12 ; hence Cl A = ].-infty,b.] ; ::_thesis: verum end; theorem Th65: :: BORSUK_5:65 for A being Subset of R^1 for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.] holds Cl A = ].-infty,b.] proof let A be Subset of R^1; ::_thesis: for a, b being real number st a < b & A = ].-infty,a.[ \/ ].a,b.] holds Cl A = ].-infty,b.] let a, b be real number ; ::_thesis: ( a < b & A = ].-infty,a.[ \/ ].a,b.] implies Cl A = ].-infty,b.] ) assume that A1: a < b and A2: A = ].-infty,a.[ \/ ].a,b.] ; ::_thesis: Cl A = ].-infty,b.] reconsider B = ].-infty,a.[, C = ].a,b.] as Subset of R^1 by TOPMETR:17; A3: Cl C = [.a,b.] by A1, Th36; Cl A = (Cl B) \/ (Cl C) by A2, PRE_TOPC:20 .= ].-infty,a.] \/ [.a,b.] by A3, Th51 .= ].-infty,b.] by A1, Th12 ; hence Cl A = ].-infty,b.] ; ::_thesis: verum end; theorem Th66: :: BORSUK_5:66 for A being Subset of R^1 for a, b, c being real number st a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds Cl A = ].-infty,c.] proof let A be Subset of R^1; ::_thesis: for a, b, c being real number st a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} holds Cl A = ].-infty,c.] let a, b, c be real number ; ::_thesis: ( a < b & b < c & A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} implies Cl A = ].-infty,c.] ) assume that A1: a < b and A2: b < c and A3: A = ((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c} ; ::_thesis: Cl A = ].-infty,c.] reconsider B = ].-infty,a.[, C = ].a,b.], D = IRRAT (b,c), E = {c} as Subset of R^1 by TOPMETR:17; A4: c in ].-infty,c.] by XXREAL_1:234; Cl A = (Cl ((B \/ C) \/ D)) \/ (Cl E) by A3, PRE_TOPC:20 .= (Cl ((B \/ C) \/ D)) \/ E by Th38 .= ((Cl (B \/ C)) \/ (Cl D)) \/ E by PRE_TOPC:20 .= (].-infty,b.] \/ (Cl D)) \/ E by A1, Th65 .= (].-infty,b.] \/ [.b,c.]) \/ E by A2, Th32 .= ].-infty,c.] \/ E by A2, Th12 .= ].-infty,c.] by A4, ZFMISC_1:40 ; hence Cl A = ].-infty,c.] ; ::_thesis: verum end; theorem :: BORSUK_5:67 for A being Subset of R^1 for a, b, c, d being real number st a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} holds Cl A = ].-infty,c.] \/ {d} proof let A be Subset of R^1; ::_thesis: for a, b, c, d being real number st a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} holds Cl A = ].-infty,c.] \/ {d} let a, b, c, d be real number ; ::_thesis: ( a < b & b < c & A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} implies Cl A = ].-infty,c.] \/ {d} ) assume that A1: a < b and A2: b < c and A3: A = (((].-infty,a.[ \/ ].a,b.]) \/ (IRRAT (b,c))) \/ {c}) \/ {d} ; ::_thesis: Cl A = ].-infty,c.] \/ {d} reconsider B = ].-infty,a.[, C = ].a,b.], D = IRRAT (b,c), E = {c}, F = {d} as Subset of R^1 by TOPMETR:17; Cl A = (Cl (((B \/ C) \/ D) \/ E)) \/ (Cl F) by A3, PRE_TOPC:20 .= (Cl (((B \/ C) \/ D) \/ E)) \/ {d} by Th38 ; hence Cl A = ].-infty,c.] \/ {d} by A1, A2, Th66; ::_thesis: verum end; theorem :: BORSUK_5:68 for A being Subset of R^1 for a, b being real number st a <= b & A = ].-infty,a.] \/ {b} holds A ` = ].a,b.[ \/ ].b,+infty.[ proof let A be Subset of R^1; ::_thesis: for a, b being real number st a <= b & A = ].-infty,a.] \/ {b} holds A ` = ].a,b.[ \/ ].b,+infty.[ let a, b be real number ; ::_thesis: ( a <= b & A = ].-infty,a.] \/ {b} implies A ` = ].a,b.[ \/ ].b,+infty.[ ) assume that A1: a <= b and A2: A = ].-infty,a.] \/ {b} ; ::_thesis: A ` = ].a,b.[ \/ ].b,+infty.[ A ` = (REAL \ ].-infty,a.]) \ {b} by A2, TOPMETR:17, XBOOLE_1:41 .= ].a,+infty.[ \ {b} by XXREAL_1:224, XXREAL_1:288 .= ].a,b.[ \/ ].b,+infty.[ by A1, XXREAL_1:365 ; hence A ` = ].a,b.[ \/ ].b,+infty.[ ; ::_thesis: verum end; theorem :: BORSUK_5:69 for a, b being real number holds [.a,+infty.[ \/ {b} <> REAL proof let a, b be real number ; ::_thesis: [.a,+infty.[ \/ {b} <> REAL set ab = (min (a,b)) - 1; A1: (min (a,b)) - 1 < min (a,b) by XREAL_1:146; min (a,b) <= b by XXREAL_0:17; then A2: not (min (a,b)) - 1 in {b} by A1, TARSKI:def_1; min (a,b) <= a by XXREAL_0:17; then (min (a,b)) - 1 < a by XREAL_1:146, XXREAL_0:2; then A3: not (min (a,b)) - 1 in [.a,+infty.[ by XXREAL_1:236; (min (a,b)) - 1 in REAL by XREAL_0:def_1; hence [.a,+infty.[ \/ {b} <> REAL by A3, A2, XBOOLE_0:def_3; ::_thesis: verum end; theorem :: BORSUK_5:70 for a, b being real number holds ].-infty,a.] \/ {b} <> REAL proof let a, b be real number ; ::_thesis: ].-infty,a.] \/ {b} <> REAL set ab = (max (a,b)) + 1; A1: (max (a,b)) + 1 > max (a,b) by XREAL_1:29; max (a,b) >= a by XXREAL_0:25; then (max (a,b)) + 1 > a by A1, XXREAL_0:2; then A2: not (max (a,b)) + 1 in ].-infty,a.] by XXREAL_1:234; max (a,b) >= b by XXREAL_0:25; then A3: not (max (a,b)) + 1 in {b} by A1, TARSKI:def_1; (max (a,b)) + 1 in REAL by XREAL_0:def_1; hence ].-infty,a.] \/ {b} <> REAL by A2, A3, XBOOLE_0:def_3; ::_thesis: verum end; theorem :: BORSUK_5:71 for TS being TopStruct for A, B being Subset of TS st A <> B holds A ` <> B ` proof let TS be TopStruct ; ::_thesis: for A, B being Subset of TS st A <> B holds A ` <> B ` let A, B be Subset of TS; ::_thesis: ( A <> B implies A ` <> B ` ) assume A1: A <> B ; ::_thesis: A ` <> B ` assume A ` = B ` ; ::_thesis: contradiction then A = (B `) ` ; hence contradiction by A1; ::_thesis: verum end; theorem :: BORSUK_5:72 for A being Subset of R^1 st REAL = A ` holds A = {} proof reconsider AB = {} R^1 as Subset of R^1 ; let A be Subset of R^1; ::_thesis: ( REAL = A ` implies A = {} ) assume REAL = A ` ; ::_thesis: A = {} then AB ` = A ` by TOPMETR:17; then AB = (A `) ` ; hence A = {} ; ::_thesis: verum end; begin theorem Th73: :: BORSUK_5:73 for X being compact Subset of R^1 for X9 being Subset of REAL st X9 = X holds ( X9 is bounded_above & X9 is bounded_below ) proof let X be compact Subset of R^1; ::_thesis: for X9 being Subset of REAL st X9 = X holds ( X9 is bounded_above & X9 is bounded_below ) let X9 be Subset of REAL; ::_thesis: ( X9 = X implies ( X9 is bounded_above & X9 is bounded_below ) ) assume X9 = X ; ::_thesis: ( X9 is bounded_above & X9 is bounded_below ) then X9 is compact by JORDAN5A:25; then X9 is real-bounded by RCOMP_1:10; hence ( X9 is bounded_above & X9 is bounded_below ) by XXREAL_2:def_11; ::_thesis: verum end; theorem Th74: :: BORSUK_5:74 for X being compact Subset of R^1 for X9 being Subset of REAL for x being real number st x in X9 & X9 = X holds ( lower_bound X9 <= x & x <= upper_bound X9 ) proof let X be compact Subset of R^1; ::_thesis: for X9 being Subset of REAL for x being real number st x in X9 & X9 = X holds ( lower_bound X9 <= x & x <= upper_bound X9 ) let X9 be Subset of REAL; ::_thesis: for x being real number st x in X9 & X9 = X holds ( lower_bound X9 <= x & x <= upper_bound X9 ) let x be real number ; ::_thesis: ( x in X9 & X9 = X implies ( lower_bound X9 <= x & x <= upper_bound X9 ) ) assume that A1: x in X9 and A2: X9 = X ; ::_thesis: ( lower_bound X9 <= x & x <= upper_bound X9 ) ( X9 is bounded_above & X9 is bounded_below ) by A2, Th73; hence ( lower_bound X9 <= x & x <= upper_bound X9 ) by A1, SEQ_4:def_1, SEQ_4:def_2; ::_thesis: verum end; theorem Th75: :: BORSUK_5:75 for C being non empty connected compact Subset of R^1 for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds [.(lower_bound C9),(upper_bound C9).] = C9 proof let C be non empty connected compact Subset of R^1; ::_thesis: for C9 being Subset of REAL st C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 holds [.(lower_bound C9),(upper_bound C9).] = C9 let C9 be Subset of REAL; ::_thesis: ( C = C9 & [.(lower_bound C9),(upper_bound C9).] c= C9 implies [.(lower_bound C9),(upper_bound C9).] = C9 ) assume that A1: C = C9 and A2: [.(lower_bound C9),(upper_bound C9).] c= C9 ; ::_thesis: [.(lower_bound C9),(upper_bound C9).] = C9 assume [.(lower_bound C9),(upper_bound C9).] <> C9 ; ::_thesis: contradiction then not C9 c= [.(lower_bound C9),(upper_bound C9).] by A2, XBOOLE_0:def_10; then consider c being set such that A3: c in C9 and A4: not c in [.(lower_bound C9),(upper_bound C9).] by TARSKI:def_3; reconsider c = c as real number by A3; A5: c <= upper_bound C9 by A1, A3, Th74; lower_bound C9 <= c by A1, A3, Th74; hence contradiction by A4, A5, XXREAL_1:1; ::_thesis: verum end; theorem Th76: :: BORSUK_5:76 for A being connected Subset of R^1 for a, b, c being real number st a <= b & b <= c & a in A & c in A holds b in A proof let A be connected Subset of R^1; ::_thesis: for a, b, c being real number st a <= b & b <= c & a in A & c in A holds b in A let a, b, c be real number ; ::_thesis: ( a <= b & b <= c & a in A & c in A implies b in A ) assume that A1: a <= b and A2: b <= c and A3: a in A and A4: c in A ; ::_thesis: b in A percases ( a = b or b = c or ( a < b & b < c & a in A & c in A ) ) by A1, A2, A3, A4, XXREAL_0:1; suppose ( a = b or b = c ) ; ::_thesis: b in A hence b in A by A3, A4; ::_thesis: verum end; supposeA5: ( a < b & b < c & a in A & c in A ) ; ::_thesis: b in A reconsider B = ].-infty,b.[, C = ].b,+infty.[ as Subset of R^1 by TOPMETR:17; assume not b in A ; ::_thesis: contradiction then A c= REAL \ {b} by TOPMETR:17, ZFMISC_1:34; then A6: A c= ].-infty,b.[ \/ ].b,+infty.[ by XXREAL_1:389; now__::_thesis:_contradiction percases ( A c= B or A c= C ) by A6, Th53, CONNSP_1:16; suppose A c= B ; ::_thesis: contradiction hence contradiction by A5, XXREAL_1:233; ::_thesis: verum end; suppose A c= C ; ::_thesis: contradiction hence contradiction by A5, XXREAL_1:235; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; theorem Th77: :: BORSUK_5:77 for A being connected Subset of R^1 for a, b being real number st a in A & b in A holds [.a,b.] c= A proof let A be connected Subset of R^1; ::_thesis: for a, b being real number st a in A & b in A holds [.a,b.] c= A let a, b be real number ; ::_thesis: ( a in A & b in A implies [.a,b.] c= A ) assume that A1: a in A and A2: b in A ; ::_thesis: [.a,b.] c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [.a,b.] or x in A ) assume x in [.a,b.] ; ::_thesis: x in A then x in { y where y is Real : ( a <= y & y <= b ) } by RCOMP_1:def_1; then ex z being Real st ( z = x & a <= z & z <= b ) ; hence x in A by A1, A2, Th76; ::_thesis: verum end; theorem Th78: :: BORSUK_5:78 for X being non empty connected compact Subset of R^1 holds X is non empty closed_interval Subset of REAL proof let C be non empty connected compact Subset of R^1; ::_thesis: C is non empty closed_interval Subset of REAL reconsider C9 = C as non empty Subset of REAL by TOPMETR:17; C is closed by COMPTS_1:7; then A1: C9 is closed by JORDAN5A:23; then A2: upper_bound C9 in C9 by Th73, RCOMP_1:12; ( C9 is bounded_below & C9 is bounded_above ) by Th73; then C9 is real-bounded by XXREAL_2:def_11; then A3: lower_bound C9 <= upper_bound C9 by SEQ_4:11; lower_bound C9 in C9 by A1, Th73, RCOMP_1:13; then [.(lower_bound C9),(upper_bound C9).] = C9 by A2, Th75, Th77; hence C is non empty closed_interval Subset of REAL by A3, MEASURE5:14; ::_thesis: verum end; theorem :: BORSUK_5:79 for A being non empty connected compact Subset of R^1 ex a, b being real number st ( a <= b & A = [.a,b.] ) proof let C be non empty connected compact Subset of R^1; ::_thesis: ex a, b being real number st ( a <= b & C = [.a,b.] ) reconsider C9 = C as non empty closed_interval Subset of REAL by Th78; A1: lower_bound C9 <= upper_bound C9 by BORSUK_4:28; A2: C9 = [.(lower_bound C9),(upper_bound C9).] by INTEGRA1:4; then A3: upper_bound C9 in C by A1, XXREAL_1:1; lower_bound C9 in C by A2, A1, XXREAL_1:1; then reconsider p1 = lower_bound C9, p2 = upper_bound C9 as Point of R^1 by A3; take p1 ; ::_thesis: ex b being real number st ( p1 <= b & C = [.p1,b.] ) take p2 ; ::_thesis: ( p1 <= p2 & C = [.p1,p2.] ) thus p1 <= p2 by BORSUK_4:28; ::_thesis: C = [.p1,p2.] thus C = [.p1,p2.] by INTEGRA1:4; ::_thesis: verum end; registration let T be TopSpace; cluster non empty open closed for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st ( b1 is open & b1 is closed & not b1 is empty ) proof reconsider F = {({} T)} as Subset-Family of T by ZFMISC_1:31; A1: F is closed proof let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in F or P is closed ) assume P in F ; ::_thesis: P is closed hence P is closed by TARSKI:def_1; ::_thesis: verum end; F is open proof let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open ) assume P in F ; ::_thesis: P is open hence P is open by TARSKI:def_1; ::_thesis: verum end; hence ex b1 being Subset-Family of T st ( b1 is open & b1 is closed & not b1 is empty ) by A1; ::_thesis: verum end; end;