borsuk_5.miz

begin

 ::$Canceled

 theorem :: BORSUK_5:2

 for x1,x2,x3,x4,x5,x6 be set holds {x1, x2, x3, x4, x5, x6} = ( {x1, x3, x6} \/ {x2, x4, x5})

 proof

 let x1,x2,x3,x4,x5,x6 be set;

 thus {x1, x2, x3, x4, x5, x6} c= ( {x1, x3, x6} \/ {x2, x4, x5})

 proof

 let x be object;

 assume x in {x1, x2, x3, x4, x5, x6};

 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 thesis by XBOOLE_0:def 3;

 end;

 let x be object;

 assume x in ( {x1, x3, x6} \/ {x2, x4, x5});

 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 thesis by ENUMSET1:def 4;

 end;

 reserve x1,x2,x3,x4,x5,x6,x7 for set;

 theorem :: BORSUK_5:3



 Th2: for x1,x2,x3,x4,x5,x6 be set st (x1,x2,x3,x4,x5,x6) are_mutually_distinct holds ( card {x1, x2, x3, x4, x5, x6}) = 6

 proof

 let x1,x2,x3,x4,x5,x6 be set;



 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_distinct ;

 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_distinct 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;

 end;

 theorem :: BORSUK_5:4

 for x1,x2,x3,x4,x5,x6,x7 be set st (x1,x2,x3,x4,x5,x6,x7) are_mutually_distinct holds ( card {x1, x2, x3, x4, x5, x6, x7}) = 7

 proof

 let x1,x2,x3,x4,x5,x6,x7 be set;



 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_distinct ;

 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_distinct 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 Th2;



 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;

 end;

 theorem :: BORSUK_5:5



 Th4: {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

 proof

 assume

 A1: {x1, x2, x3} misses {x4, x5, 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;

 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 thesis by A1, A3, A2, A4, XBOOLE_0: 3;

 end;

 theorem :: BORSUK_5:6

 (x1,x2,x3) are_mutually_distinct & (x4,x5,x6) are_mutually_distinct & {x1, x2, x3} misses {x4, x5, x6} implies (x1,x2,x3,x4,x5,x6) are_mutually_distinct

 proof

 assume that

 A1: (x1,x2,x3) are_mutually_distinct and

 A2: (x4,x5,x6) are_mutually_distinct and

 A3: {x1, x2, x3} misses {x4, x5, x6};



 A4: x1 <> x2 by A1, ZFMISC_1:def 5;



 A5: x3 <> x5 by A3, Th4;



 A6: x3 <> x4 by A3, Th4;



 A7: x1 <> x6 by A3, Th4;



 A8: x1 <> x3 by A1, ZFMISC_1:def 5;



 A9: x2 <> x5 by A3, Th4;



 A10: x5 <> x6 by A2, ZFMISC_1:def 5;



 A11: x2 <> x4 by A3, Th4;



 A12: x4 <> x5 by A2, ZFMISC_1:def 5;



 A13: x2 <> x6 by A3, Th4;



 A14: x4 <> x6 by A2, ZFMISC_1:def 5;



 A15: x3 <> x6 by A3, Th4;



 A16: x1 <> x5 by A3, Th4;



 A17: x2 <> x3 by A1, ZFMISC_1:def 5;

 x1 <> x4 by A3, Th4;

 hence thesis by A4, A17, A8, A12, A10, A14, A16, A7, A11, A9, A13, A6, A5, A15, ZFMISC_1:def 8;

 end;

 theorem :: BORSUK_5:7

 (x1,x2,x3,x4,x5,x6) are_mutually_distinct & {x1, x2, x3, x4, x5, x6} misses {x7} implies (x1,x2,x3,x4,x5,x6,x7) are_mutually_distinct

 proof

 assume that

 A1: (x1,x2,x3,x4,x5,x6) are_mutually_distinct and

 A2: {x1, x2, x3, x4, x5, x6} misses {x7};



 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 thesis 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;

 end;

 theorem :: BORSUK_5:8

 (x1,x2,x3,x4,x5,x6,x7) are_mutually_distinct implies (x7,x1,x2,x3,x4,x5,x6) are_mutually_distinct

 proof

 assume

 A1: (x1,x2,x3,x4,x5,x6,x7) are_mutually_distinct ;

 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 thesis 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;

 end;

 theorem :: BORSUK_5:9

 (x1,x2,x3,x4,x5,x6,x7) are_mutually_distinct implies (x1,x2,x5,x3,x6,x7,x4) are_mutually_distinct

 proof

 assume

 A1: (x1,x2,x3,x4,x5,x6,x7) are_mutually_distinct ;

 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 thesis 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;

 end;



 Lm1: R^1 is pathwise_connected

 proof

 let a,b be Point of R^1 ;

 per cases ;

 suppose

 A1: a <= b;

 reconsider B = [.a, b.] as Subset of R^1 by TOPMETR: 17;

 reconsider 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 as Function of I[01] , R^1 ;

 take g;

 ( 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;

 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;

 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;

 end;

 suppose

 A3: b <= a;

 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 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;

 then

 reconsider P = g as Path of b, a by A7, A5, A6, BORSUK_2:def 2;

 take ( - P);

 ex t be 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 ;

 hence thesis by BORSUK_2:def 2;

 end;

 end;

 registration

 cluster R^1 -> pathwise_connected;

 coherence by Lm1;

 end

 registration

 cluster connected non empty for TopSpace;

 existence

 proof

 take R^1 ;

 thus thesis;

 end;

 end

 begin

 theorem :: BORSUK_5:10

 for A,B be Subset of R^1 , a,b,c,d be Real 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 , a,b,c,d be Real;

 assume that

 A1: a < b and

 A2: b <= c and

 A3: c < d and

 A4: A = [.a, b.[ and

 A5: B = ].c, d.];

 ( 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 thesis by A6, CONNSP_1:def 1;

 end;

 theorem :: BORSUK_5:11



 Th10: for a,b,c be Real st a <= c & c <= b holds ( [.a, b.] \/ [.c, +infty .[) = [.a, +infty .[

 proof

 let a,b,c be Real;

 assume that

 A1: a <= c and

 A2: c <= b;



 A3: [.a, +infty .[ c= ( [.a, b.] \/ [.c, +infty .[)

 proof

 let r be object;

 assume

 A4: r in [.a, +infty .[;

 then

 reconsider s = r as Real;



 A5: a <= s by A4, XXREAL_1: 236;

 per cases ;

 suppose s <= b;

 then s in [.a, b.] by A5, XXREAL_1: 1;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose not s <= b;

 then c <= s by A2, XXREAL_0: 2;

 then s in [.c, +infty .[ by XXREAL_1: 236;

 hence thesis by XBOOLE_0:def 3;

 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 thesis by A3, XBOOLE_0:def 10;

 end;

 theorem :: BORSUK_5:12



 Th11: for a,b,c be Real st a <= c & c <= b holds ( ]. -infty , c.] \/ [.a, b.]) = ]. -infty , b.]

 proof

 let a,b,c be Real;

 assume that

 A1: a <= c and

 A2: c <= b;

 thus ( ]. -infty , c.] \/ [.a, b.]) c= ]. -infty , b.]

 proof

 let x be object;

 assume

 A3: x in ( ]. -infty , c.] \/ [.a, b.]);

 then

 reconsider x as Real;

 per cases by A3, XBOOLE_0:def 3;

 suppose x in ]. -infty , c.];

 then x <= c by XXREAL_1: 234;

 then x <= b by A2, XXREAL_0: 2;

 hence thesis by XXREAL_1: 234;

 end;

 suppose x in [.a, b.];

 then x <= b by XXREAL_1: 1;

 hence thesis by XXREAL_1: 234;

 end;

 end;

 let x be object;

 assume

 A4: x in ]. -infty , b.];

 then

 reconsider x as Real;

 per cases ;

 suppose x <= c;

 then x in ]. -infty , c.] by XXREAL_1: 234;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose

 A5: x > c;



 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 thesis by XBOOLE_0:def 3;

 end;

 end;

 registration

 cluster -> real for Element of RAT ;

 coherence ;

 end

 theorem :: BORSUK_5:13

 for A be Subset of R^1 , p be Point of RealSpace holds p in ( Cl A) iff for r be Real st r > 0 holds ( Ball (p,r)) meets A by GOBOARD6: 92, TOPMETR:def 6;

 theorem :: BORSUK_5:14



 Th13: for p,q be Element of RealSpace st q >= p holds ( dist (p,q)) = (q - p)

 proof

 let p,q be Element of RealSpace ;

 assume p <= q;

 then

 A1: (q - p) >= 0 by XREAL_1: 48;

 ( dist (p,q)) = |.(q - p).| by TOPMETR: 11

 .= (q - p) by A1, ABSVALUE:def 1;

 hence thesis;

 end;

 theorem :: BORSUK_5:15



 Th14: for A be Subset of R^1 st A = RAT holds ( Cl A) = the carrier of R^1

 proof

 let A be Subset of R^1 ;

 assume

 A1: A = RAT ;

 the carrier of R^1 c= ( Cl A)

 proof

 let x be object;

 assume x in the carrier of R^1 ;

 then

 reconsider p = x as Element of RealSpace by METRIC_1:def 13, TOPMETR: 17;

 now

 let r be Real;

 reconsider pr = (p + r) as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 assume r > 0 ;

 then

 consider Q be Rational 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, Th13;

 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;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 hence thesis by XBOOLE_0:def 10;

 end;

 theorem :: BORSUK_5:16



 Th15: for A be Subset of R^1 , a,b be Real st A = ].a, b.[ & a <> b holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: A = ].a, b.[ and

 A2: a <> b;

 ( Cl ].a, b.[) = [.a, b.] by A2, JORDAN5A: 26;

 hence thesis by A1, JORDAN5A: 24;

 end;

 begin

 registration

 cluster number_e -> irrational;

 coherence by IRRAT_1: 41;

 end

 definition

 :: BORSUK_5:def1

 func IRRAT -> Subset of REAL equals ( REAL \ RAT );

 coherence ;

 end

 definition

 let a,b be Real;

 :: BORSUK_5:def2

 func RAT (a,b) -> Subset of REAL equals ( RAT /\ ].a, b.[);

 coherence ;

 :: BORSUK_5:def3

 func IRRAT (a,b) -> Subset of REAL equals ( IRRAT /\ ].a, b.[);

 coherence ;

 end

 theorem :: BORSUK_5:17



 Th16: for x be Real holds x is irrational iff x in IRRAT

 proof

 let x be Real;



 A1: x in REAL by XREAL_0:def 1;

 hereby

 assume x is irrational;

 then not x in RAT ;

 hence x in IRRAT by A1, XBOOLE_0:def 5;

 end;

 assume x in IRRAT ;

 then not x in RAT by XBOOLE_0:def 5;

 hence thesis by RAT_1:def 2;

 end;

 registration

 cluster irrational for Real;

 existence by IRRAT_1: 41;

 end

 registration

 cluster IRRAT -> non empty;

 coherence by Th16, IRRAT_1: 41;

 end

 registration

 let a be Rational, b be irrational Real;

 cluster (a + b) -> irrational;

 coherence

 proof

 set m1 = the Integer;

 assume (a + b) is rational;

 then

 consider m,n be Integer such that n <> 0 and

 A1: (a + b) = (m / n) by RAT_1: 2;

 ((a + b) - a) = (((m * m1) - (m1 * n)) / (m1 * n)) by A1;

 hence thesis;

 end;

 cluster (b + a) -> irrational;

 coherence ;

 end

 theorem :: BORSUK_5:18

 for a be Rational, b be irrational Real holds (a + b) is irrational;

 registration

 let a be irrational Real;

 cluster ( - a) -> irrational;

 coherence

 proof

 assume ( - a) is rational;

 then

 reconsider b = ( - a) as Rational;

 ( - b) is rational;

 hence thesis;

 end;

 end

 theorem :: BORSUK_5:19

 for a be irrational Real holds ( - a) is irrational;

 registration

 let a be Rational, b be irrational Real;

 cluster (a - b) -> irrational;

 coherence

 proof

 (a + ( - b)) is irrational;

 hence thesis;

 end;

 cluster (b - a) -> irrational;

 coherence

 proof

 (b + ( - a)) is irrational;

 hence thesis;

 end;

 end

 theorem :: BORSUK_5:20

 for a be Rational, b be irrational Real holds (a - b) is irrational;

 theorem :: BORSUK_5:21

 for a be Rational, b be irrational Real holds (b - a) is irrational;

 theorem :: BORSUK_5:22



 Th21: for a be Rational, b be irrational Real st a <> 0 holds (a * b) is irrational

 proof

 let a be Rational, b be irrational Real;

 assume

 A1: a <> 0 ;

 assume (a * b) is rational;

 then

 consider m,n be Integer such that n <> 0 and

 A2: (a * b) = (m / n) by RAT_1: 2;

 consider m1,n1 be 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 thesis by A1, XCMPLX_1: 89;

 end;

 theorem :: BORSUK_5:23



 Th22: for a be Rational, b be irrational Real st a <> 0 holds (b / a) is irrational

 proof

 let a be Rational, b be irrational Real;

 assume

 A1: a <> 0 ;

 assume (b / a) is rational;

 then

 reconsider c = (b / a) as Rational;

 (c * a) is rational;

 hence thesis by A1, XCMPLX_1: 87;

 end;

 registration

 cluster irrational -> non zero for Real;

 coherence ;

 end

 theorem :: BORSUK_5:24



 Th23: for a be Rational, b be irrational Real st a <> 0 holds (a / b) is irrational

 proof

 let a be Rational, b be irrational Real;

 assume

 A1: a <> 0 ;

 assume (a / b) is rational;

 then

 reconsider c = (a / b) as Rational;

 (c * b) is irrational by A1, Th21, XCMPLX_1: 50;

 hence thesis by XCMPLX_1: 87;

 end;

 registration

 let r be irrational Real;

 cluster ( frac r) -> irrational;

 coherence

 proof

 ( frac r) = (r - [\r/]) by INT_1:def 8;

 hence thesis;

 end;

 end

 theorem :: BORSUK_5:25

 for r be irrational Real holds ( frac r) is irrational;

 registration

 cluster non zero for Rational;

 existence

 proof

 1 <> 0 ;

 hence thesis;

 end;

 end

 registration

 let a be non zero Rational, b be irrational Real;

 cluster (a * b) -> irrational;

 coherence by Th21;

 cluster (b * a) -> irrational;

 coherence ;

 cluster (a / b) -> irrational;

 coherence by Th23;

 cluster (b / a) -> irrational;

 coherence by Th22;

 end

 theorem :: BORSUK_5:26



 Th25: for a,b be Real st a < b holds ex p1,p2 be Rational st a < p1 & p1 < p2 & p2 < b

 proof

 let a,b be Real;

 assume a < b;

 then

 consider p1 be Rational such that

 A1: a < p1 and

 A2: p1 < b by RAT_1: 7;

 ex p2 be Rational st p1 < p2 & p2 < b by A2, RAT_1: 7;

 hence thesis by A1;

 end;

 theorem :: BORSUK_5:27



 Th26: for a,b be Real st a < b holds ex p be irrational Real st a < p & p < b

 proof

 set x = ( frac number_e );

 let a,b be Real;



 A1: x < 1 by INT_1: 43;

 assume a < b;

 then

 consider p1,p2 be Rational such that

 A2: a < p1 and

 A3: p1 < p2 and

 A4: p2 p1 by A3, A5, A1, XREAL_1: 177;

 then

 A7: y > a by A2, XXREAL_0: 2;



 A8: y = (p1 + (x * (p2 - p1)));

 (p2 - p1) <> 0 by A3;

 hence thesis by A8, A6, A7;

 end;

 theorem :: BORSUK_5:28



 Th27: for A be Subset of R^1 st A = IRRAT holds ( Cl A) = the carrier of R^1

 proof

 let A be Subset of R^1 ;

 assume

 A1: A = IRRAT ;

 the carrier of R^1 c= ( Cl A)

 proof

 let x be object;

 assume x in the carrier of R^1 ;

 then

 reconsider p = x as Element of RealSpace by METRIC_1:def 13, TOPMETR: 17;

 now

 let r be Real;

 reconsider pr = (p + r) as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 assume r > 0 ;

 then

 consider Q be irrational Real such that

 A2: p < Q and

 A3: Q < pr by Th26, 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, Th13;

 then

 A4: P in ( Ball (p,r)) by METRIC_1: 11;

 Q in A by A1, Th16;

 hence ( Ball (p,r)) meets A by A4, XBOOLE_0: 3;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 hence thesis by XBOOLE_0:def 10;

 end;



 Lm2: for A be Subset of R^1 , a,b be Real st a < b & A = ( RAT (a,b)) holds a in ( Cl A) & b in ( Cl A)

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a 0 holds ( Ball (a9,r)) meets A

 proof

 set p = a;

 let r be Real;

 reconsider pp = (a + r) as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 set pr = ( min (pp,((p + b) / 2)));



 A3: pr <= ((p + b) / 2) by XXREAL_0: 17;

 assume

 A4: r > 0 ;

 p < pr

 proof

 per cases by XXREAL_0: 15;

 suppose pr = pp;

 hence thesis by A4, XREAL_1: 29;

 end;

 suppose pr = ((p + b) / 2);

 hence thesis by A1, XREAL_1: 226;

 end;

 end;

 then

 consider Q be Rational such that

 A5: p < Q and

 A6: Q < pr by RAT_1: 7;

 ((p + b) / 2) < b by A1, XREAL_1: 226;

 then pr < 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;

 pr <= pp by XXREAL_0: 17;

 then

 A8: (pr - 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) < (pr - p) by A6, XREAL_1: 9;

 then (P - p) < r by A8, XXREAL_0: 2;

 then ( dist (a9,P)) < r by A5, Th13;

 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 thesis by A9, XBOOLE_0: 3;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 b in ( Cl A)

 proof

 reconsider a9 = b as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 for r be Real st r > 0 holds ( Ball (a9,r)) meets A

 proof

 set p = b;

 let r be Real;

 reconsider pp = (b - r) as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 set pr = ( max (pp,((p + a) / 2)));



 A10: pr >= ((p + a) / 2) by XXREAL_0: 25;

 assume r > 0 ;

 then

 A11: b < (b + r) by XREAL_1: 29;

 p > pr

 proof

 per cases by XXREAL_0: 16;

 suppose pr = pp;

 hence thesis by A11, XREAL_1: 19;

 end;

 suppose pr = ((p + a) / 2);

 hence thesis by A1, XREAL_1: 226;

 end;

 end;

 then

 consider Q be Rational such that

 A12: pr < Q and

 A13: Q a by A1, XREAL_1: 226;

 then a < pr by A10, XXREAL_0: 2;

 then a < Q by A12, XXREAL_0: 2;

 then

 A14: Q in ].a, b.[ by A13, XXREAL_1: 4;

 pr >= pp by XXREAL_0: 25;

 then

 A15: (p - pr) <= (p - pp) by XREAL_1: 13;

 reconsider P = Q as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 (p - P) < (p - pr) by A12, XREAL_1: 10;

 then (p - P) < r by A15, XXREAL_0: 2;

 then ( dist (a9,P)) < r by A13, Th13;

 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 thesis by A16, XBOOLE_0: 3;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 hence thesis;

 end;



 Lm3: for A be Subset of R^1 , a,b be Real st a < b & A = ( IRRAT (a,b)) holds a in ( Cl A) & b in ( Cl A)

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a 0 holds ( Ball (a9,r)) meets A

 proof

 set p = a;

 let r be Real;

 reconsider pp = (a + r) as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 set pr = ( min (pp,((p + b) / 2)));



 A3: pr <= ((p + b) / 2) by XXREAL_0: 17;

 assume

 A4: r > 0 ;

 p < pr

 proof

 per cases by XXREAL_0: 15;

 suppose pr = pp;

 hence thesis by A4, XREAL_1: 29;

 end;

 suppose pr = ((p + b) / 2);

 hence thesis by A1, XREAL_1: 226;

 end;

 end;

 then

 consider Q be irrational Real such that

 A5: p < Q and

 A6: Q < pr by Th26;

 ((p + b) / 2) < b by A1, XREAL_1: 226;

 then pr < 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;

 pr <= pp by XXREAL_0: 17;

 then

 A8: (pr - 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) < (pr - p) by A6, XREAL_1: 9;

 then (P - p) < r by A8, XXREAL_0: 2;

 then ( dist (a9,P)) < r by A5, Th13;

 then

 A9: P in ( Ball (a9,r)) by METRIC_1: 11;

 Q in IRRAT by Th16;

 then Q in A by A2, A7, XBOOLE_0:def 4;

 hence thesis by A9, XBOOLE_0: 3;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 b in ( Cl A)

 proof

 reconsider a9 = b as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 for r be Real st r > 0 holds ( Ball (a9,r)) meets A

 proof

 set p = b;

 let r be Real;

 reconsider pp = (b - r) as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 set pr = ( max (pp,((p + a) / 2)));



 A10: pr >= ((p + a) / 2) by XXREAL_0: 25;

 assume r > 0 ;

 then

 A11: b < (b + r) by XREAL_1: 29;

 p > pr

 proof

 per cases by XXREAL_0: 16;

 suppose pr = pp;

 hence thesis by A11, XREAL_1: 19;

 end;

 suppose pr = ((p + a) / 2);

 hence thesis by A1, XREAL_1: 226;

 end;

 end;

 then

 consider Q be irrational Real such that

 A12: pr < Q and

 A13: Q a by A1, XREAL_1: 226;

 then a < pr by A10, XXREAL_0: 2;

 then a < Q by A12, XXREAL_0: 2;

 then

 A14: Q in ].a, b.[ by A13, XXREAL_1: 4;

 pr >= pp by XXREAL_0: 25;

 then

 A15: (p - pr) <= (p - pp) by XREAL_1: 13;

 reconsider P = Q as Element of RealSpace by METRIC_1:def 13, XREAL_0:def 1;

 (p - P) < (p - pr) by A12, XREAL_1: 10;

 then (p - P) < r by A15, XXREAL_0: 2;

 then ( dist (a9,P)) < r by A13, Th13;

 then

 A16: P in ( Ball (a9,r)) by METRIC_1: 11;

 Q in IRRAT by Th16;

 then Q in A by A2, A14, XBOOLE_0:def 4;

 hence thesis by A16, XBOOLE_0: 3;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 hence thesis;

 end;

 theorem :: BORSUK_5:29



 Th28: for a,b,c be Real holds c in ( RAT (a,b)) iff c is rational & a < c & c < b

 proof

 let a,b,c be Real;

 hereby

 assume

 A1: c in ( RAT (a,b));

 then c in ].a, b.[ by XBOOLE_0:def 4;

 hence c is rational & a < c & c < b by A1, XXREAL_1: 4;

 end;

 assume that

 A2: c is rational and

 A3: a < c and

 A4: c < b;



 A5: c in RAT by A2, RAT_1:def 2;

 c in ].a, b.[ by A3, A4, XXREAL_1: 4;

 hence thesis by A5, XBOOLE_0:def 4;

 end;

 theorem :: BORSUK_5:30



 Th29: for a,b,c be Real holds c in ( IRRAT (a,b)) iff c is irrational & a < c & c < b

 proof

 let a,b,c be Real;

 hereby

 assume

 A1: c in ( IRRAT (a,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, Th16, XXREAL_1: 4;

 end;

 assume that

 A3: c is irrational and

 A4: a < c and

 A5: c < b;



 A6: c in ].a, b.[ by A4, A5, XXREAL_1: 4;

 c in IRRAT by A3, Th16;

 hence thesis by A6, XBOOLE_0:def 4;

 end;

 theorem :: BORSUK_5:31



 Th30: for A be Subset of R^1 , a,b be Real st a < b & A = ( RAT (a,b)) holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ( RAT (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.]

 proof

 let x be object;

 assume x in ( Cl A);

 then x in (( Cl RT) /\ ( Cl ab)) by A2, A4;

 then x in (the carrier of R^1 /\ ( Cl ab)) by Th14;

 hence thesis by A1, A3, Th15;

 end;

 thus [.a, b.] c= ( Cl A)

 proof

 let x be object;

 assume

 A5: x in [.a, b.];

 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;

 per cases by A7, XXREAL_0: 1;

 suppose

 A8: p < b;

 now

 let r be Real;

 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: pr <= ((p + b) / 2) by XXREAL_0: 17;

 assume

 A10: r > 0 ;

 p < pr

 proof

 per cases by XXREAL_0: 15;

 suppose pr = pp;

 hence thesis by A10, XREAL_1: 29;

 end;

 suppose pr = ((p + b) / 2);

 hence thesis by A8, XREAL_1: 226;

 end;

 end;

 then

 consider Q be Rational such that

 A11: p < Q and

 A12: Q < pr by RAT_1: 7;

 ((p + b) / 2) < b by A8, XREAL_1: 226;

 then pr < b by A9, XXREAL_0: 2;

 then

 A13: Q < b by A12, XXREAL_0: 2;

 pr <= pp by XXREAL_0: 17;

 then

 A14: (pr - 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) < (pr - p) by A12, XREAL_1: 9;

 then (P - p) < r by A14, XXREAL_0: 2;

 then ( dist (p,P)) < r by A11, Th13;

 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;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 suppose p = b;

 hence thesis by A1, A2, Lm2;

 end;

 end;

 end;

 theorem :: BORSUK_5:32



 Th31: for A be Subset of R^1 , a,b be Real st a < b & A = ( IRRAT (a,b)) holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ( IRRAT (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.]

 proof

 let x be object;

 assume x in ( Cl A);

 then x in (( Cl RT) /\ ( Cl ab)) by A2, A4;

 then x in (the carrier of R^1 /\ ( Cl ab)) by Th27;

 hence thesis by A1, A3, Th15;

 end;

 thus [.a, b.] c= ( Cl A)

 proof

 let x be object;

 assume

 A5: x in [.a, b.];

 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;

 per cases by A7, XXREAL_0: 1;

 suppose

 A8: p < b;

 now

 let r be Real;

 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: pr <= ((p + b) / 2) by XXREAL_0: 17;

 assume

 A10: r > 0 ;

 p < pr

 proof

 per cases by XXREAL_0: 15;

 suppose pr = pp;

 hence thesis by A10, XREAL_1: 29;

 end;

 suppose pr = ((p + b) / 2);

 hence thesis by A8, XREAL_1: 226;

 end;

 end;

 then

 consider Q be irrational Real such that

 A11: p < Q and

 A12: Q < pr by Th26;

 ((p + b) / 2) < b by A8, XREAL_1: 226;

 then pr < b by A9, XXREAL_0: 2;

 then

 A13: Q < b by A12, XXREAL_0: 2;

 pr <= pp by XXREAL_0: 17;

 then

 A14: (pr - 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) < (pr - p) by A12, XREAL_1: 9;

 then (P - p) < r by A14, XXREAL_0: 2;

 then ( dist (p,P)) < r by A11, Th13;

 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 Th16;

 then Q in A by A2, A16, XBOOLE_0:def 4;

 hence ( Ball (p,r)) meets A by A15, XBOOLE_0: 3;

 end;

 hence thesis by GOBOARD6: 92, TOPMETR:def 6;

 end;

 suppose p = b;

 hence thesis by A1, A2, Lm3;

 end;

 end;

 end;

 theorem :: BORSUK_5:33



 Th32: for T be connected TopSpace, A be closed open Subset of T holds A = {} or A = ( [#] T)

 proof

 let T be connected TopSpace, A be closed open Subset of T;

 assume that

 A1: A <> {} and

 A2: A <> ( [#] T);



 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 thesis by CONNSP_1: 27;

 end;

 theorem :: BORSUK_5:34



 Th33: for A be Subset of R^1 st A is closed open holds A = {} or A = REAL

 proof

 let A be Subset of R^1 ;

 assume A is closed open;

 then

 reconsider A as closed open Subset of R^1 ;

 A = {} or A = ( [#] R^1 ) by Th32;

 hence thesis by TOPMETR: 17;

 end;

 begin

 theorem :: BORSUK_5:35



 Th34: for A be Subset of R^1 , a,b be Real st A = [.a, b.[ & a <> b holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: A = [.a, b.[ and

 A2: a <> b;

 ( Cl [.a, b.[) = [.a, b.] by A2, BORSUK_4: 12;

 hence thesis by A1, JORDAN5A: 24;

 end;

 theorem :: BORSUK_5:36



 Th35: for A be Subset of R^1 , a,b be Real st A = ].a, b.] & a <> b holds ( Cl A) = [.a, b.]

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: A = ].a, b.] and

 A2: a <> b;

 ( Cl ].a, b.]) = [.a, b.] by A2, BORSUK_4: 11;

 hence thesis by A1, JORDAN5A: 24;

 end;

 theorem :: BORSUK_5:37

 for A be Subset of R^1 , a,b,c be Real st A = ( [.a, b.[ \/ ].b, c.]) & a < b & b < c holds ( Cl A) = [.a, c.]

 proof

 let A be Subset of R^1 , a,b,c be Real;

 assume that

 A1: A = ( [.a, b.[ \/ ].b, c.]) and

 A2: a < b and

 A3: b < 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, Th34

 .= ( [.a, b.] \/ [.b, c.]) by A3, Th35

 .= [.a, c.] by A2, A3, XXREAL_1: 174;

 hence thesis;

 end;

 theorem :: BORSUK_5:38



 Th37: for A be Subset of R^1 , a be Real st A = {a} holds ( Cl A) = {a}

 proof

 let A be Subset of R^1 , a be Real;



 A1: a is Point of R^1 by TOPMETR: 17, XREAL_0:def 1;

 assume A = {a};

 hence thesis by A1, YELLOW_8: 26;

 end;

 theorem :: BORSUK_5:39



 Th38: for A be Subset of REAL , B be Subset of R^1 st A = B holds A is open iff B is open

 proof

 let A be Subset of REAL , B be Subset of R^1 ;

 assume

 A1: A = B;

 hereby

 assume A 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;

 end;

 assume B 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 thesis by JORDAN5A: 5;

 end;



 Lm4: for a be Real holds ]. -infty , a.] is closed

 proof

 let a be Real;

 ]. -infty , a.] = ( left_closed_halfline a);

 hence thesis;

 end;



 Lm5: for a be Real holds [.a, +infty .[ is closed

 proof

 let a be Real;

 [.a, +infty .[ = ( right_closed_halfline a);

 hence thesis;

 end;

 registration

 let A,B be open Subset of REAL ;

 reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR: 17;

 cluster (A /\ B) -> open;

 coherence

 proof



 A1: B1 is open by Th38;

 A1 is open by Th38;

 then (A1 /\ B1) is open by A1;

 hence thesis by Th38;

 end;

 cluster (A \/ B) -> open;

 coherence

 proof



 A2: B1 is open by Th38;

 A1 is open by Th38;

 then (A1 \/ B1) is open by A2;

 hence thesis by Th38;

 end;

 end



 Lm6: for a,b be ExtReal holds ].a, b.[ is open

 proof

 let a,b be ExtReal;

 set A = ].a, b.[;

 per cases by XXREAL_0: 14;

 suppose a in REAL & b in REAL ;

 then

 reconsider a, b as Real;

 A = ( ]. -infty , b.[ /\ ].a, +infty .[) by XXREAL_1: 269;

 hence thesis;

 end;

 suppose a = +infty ;

 then A = {} by XXREAL_1: 214;

 hence thesis;

 end;

 suppose that

 A1: a = -infty and

 A2: b in REAL ;

 reconsider b as Real by A2;

 A = ( left_open_halfline b) by A1;

 hence thesis;

 end;

 suppose that

 A3: a in REAL and

 A4: b = +infty ;

 reconsider a as Real by A3;

 A = ( right_open_halfline a) by A4;

 hence thesis;

 end;

 suppose b = -infty ;

 then A = {} by XXREAL_1: 210;

 hence thesis;

 end;

 suppose a = -infty & b = +infty ;

 then A = ( [#] REAL ) by XXREAL_1: 224;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_5:40



 Th39: for A be Subset of R^1 , a,b be ExtReal st A = ].a, b.[ holds A is open

 proof

 let A be Subset of R^1 , a,b be ExtReal;

 ].a, b.[ is open by Lm6;

 hence thesis by Th38;

 end;

 theorem :: BORSUK_5:41



 Th40: for A be Subset of R^1 , a be Real st A = ]. -infty , a.] holds A is closed

 proof

 let A be Subset of R^1 , a be Real;

 assume

 A1: A = ]. -infty , a.];

 ]. -infty , a.] is closed by Lm4;

 hence thesis by A1, JORDAN5A: 23;

 end;

 theorem :: BORSUK_5:42



 Th41: for A be Subset of R^1 , a be Real st A = [.a, +infty .[ holds A is closed

 proof

 let A be Subset of R^1 , a be Real;

 assume

 A1: A = [.a, +infty .[;

 [.a, +infty .[ is closed by Lm5;

 hence thesis by A1, JORDAN5A: 23;

 end;

 theorem :: BORSUK_5:43



 Th42: for a be Real holds [.a, +infty .[ = ( {a} \/ ].a, +infty .[)

 proof

 let a be Real;

 thus [.a, +infty .[ c= ( {a} \/ ].a, +infty .[)

 proof

 let x be object;

 assume

 A1: x in [.a, +infty .[;

 then

 reconsider x as Real;



 A2: x >= a by A1, XXREAL_1: 236;

 per cases by A2, XXREAL_0: 1;

 suppose x = a;

 then x in {a} by TARSKI:def 1;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose x > a;

 then x in ].a, +infty .[ by XXREAL_1: 235;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 let x be object;

 assume

 A3: x in ( {a} \/ ].a, +infty .[);

 then

 reconsider x as Real;

 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 thesis by XXREAL_1: 236;

 end;

 theorem :: BORSUK_5:44



 Th43: for a be Real holds ]. -infty , a.] = ( {a} \/ ]. -infty , a.[)

 proof

 let a be Real;

 thus ]. -infty , a.] c= ( {a} \/ ]. -infty , a.[)

 proof

 let x be object;

 assume

 A1: x in ]. -infty , a.];

 then

 reconsider x as Real;



 A2: x <= a by A1, XXREAL_1: 234;

 per cases by A2, XXREAL_0: 1;

 suppose x = a;

 then x in {a} by TARSKI:def 1;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose x < a;

 then x in ]. -infty , a.[ by XXREAL_1: 233;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 let x be object;

 assume

 A3: x in ( {a} \/ ]. -infty , a.[);

 then

 reconsider x as Real;

 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 thesis by XXREAL_1: 234;

 end;

 registration

 let a be Real;

 cluster ].a, +infty .[ -> non empty;

 coherence

 proof

 a < (a + 1) by XREAL_1: 29;

 hence thesis by XXREAL_1: 235;

 end;

 cluster ]. -infty , a.] -> non empty;

 coherence by XXREAL_1: 234;

 cluster ]. -infty , a.[ -> non empty;

 coherence

 proof

 (a - 1) < a by XREAL_1: 146;

 hence thesis by XXREAL_1: 233;

 end;

 cluster [.a, +infty .[ -> non empty;

 coherence by XXREAL_1: 236;

 end

 theorem :: BORSUK_5:45



 Th44: for a be Real holds ].a, +infty .[ <> REAL by XREAL_0:def 1, XXREAL_1: 235;

 theorem :: BORSUK_5:46

 for a be Real holds [.a, +infty .[ <> REAL

 proof

 let a be Real;



 A1: (a - 1) < a by XREAL_1: 146;

 (a - 1) in REAL by XREAL_0:def 1;

 hence thesis by A1, XXREAL_1: 236;

 end;

 theorem :: BORSUK_5:47

 for a be Real holds ]. -infty , a.] <> REAL

 proof

 let a be Real;



 A1: (a + 1) > a by XREAL_1: 29;

 (a + 1) in REAL by XREAL_0:def 1;

 hence thesis by A1, XXREAL_1: 234;

 end;

 theorem :: BORSUK_5:48



 Th47: for a be Real holds ]. -infty , a.[ <> REAL by XREAL_0:def 1, XXREAL_1: 233;

 theorem :: BORSUK_5:49



 Th48: for A be Subset of R^1 , a be Real st A = ].a, +infty .[ holds ( Cl A) = [.a, +infty .[

 proof

 let A be Subset of R^1 , a be Real;

 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 .[;

 then

 A2: A9 is open by Th39;

 C is closed by Th41;

 then

 A3: ( Cl A9) c= C by A1, TOPS_1: 5, XXREAL_1: 45;



 A4: C = (A9 \/ {a}) by A1, Th42;

 per cases by A4, A3, PRE_TOPC: 18, ZFMISC_1: 138;

 suppose ( Cl A9) = C;

 hence thesis;

 end;

 suppose ( Cl A9) = A9;

 hence thesis by A1, A2, Th33, Th44;

 end;

 end;

 theorem :: BORSUK_5:50

 for a be Real holds ( Cl ].a, +infty .[) = [.a, +infty .[

 proof

 let a be Real;

 reconsider A = ].a, +infty .[ as Subset of R^1 by TOPMETR: 17;

 ( Cl A) = [.a, +infty .[ by Th48;

 hence thesis by JORDAN5A: 24;

 end;

 theorem :: BORSUK_5:51



 Th50: for A be Subset of R^1 , a be Real st A = ]. -infty , a.[ holds ( Cl A) = ]. -infty , a.]

 proof

 let A be Subset of R^1 , a be Real;

 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.[;

 then

 A2: A9 is open by Th39;

 C is closed by Th40;

 then

 A3: ( Cl A9) c= C by A1, TOPS_1: 5, XXREAL_1: 41;



 A4: C = (A9 \/ {a}) by A1, Th43;

 per cases by A4, A3, PRE_TOPC: 18, ZFMISC_1: 138;

 suppose ( Cl A9) = C;

 hence thesis;

 end;

 suppose ( Cl A9) = A9;

 hence thesis by A1, A2, Th33, Th47;

 end;

 end;

 theorem :: BORSUK_5:52

 for a be Real holds ( Cl ]. -infty , a.[) = ]. -infty , a.]

 proof

 let a be Real;

 reconsider A = ]. -infty , a.[ as Subset of R^1 by TOPMETR: 17;

 ( Cl A) = ]. -infty , a.] by Th50;

 hence thesis by JORDAN5A: 24;

 end;

 theorem :: BORSUK_5:53



 Th52: for A,B be Subset of R^1 , b be Real st A = ]. -infty , b.[ & B = ].b, +infty .[ holds (A,B) are_separated

 proof

 let A,B be Subset of R^1 , b be Real;

 assume that

 A1: A = ]. -infty , b.[ and

 A2: B = ].b, +infty .[;

 ( Cl B) = [.b, +infty .[ by A2, Th48;

 then

 A3: ( Cl B) misses A by A1, XXREAL_1: 94;

 ( Cl A) = ]. -infty , b.] by A1, Th50;

 then ( Cl A) misses B by A2, XXREAL_1: 91;

 hence thesis by A3, CONNSP_1:def 1;

 end;

 theorem :: BORSUK_5:54

 for A be Subset of R^1 , a,b be Real st a < b & A = ( [.a, b.[ \/ ].b, +infty .[) holds ( Cl A) = [.a, +infty .[

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ( [.a, b.[ \/ ].b, +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 Th48;

 ( Cl B) = [.a, b.] by A1, Th34;

 hence thesis by A1, A4, A3, Th10;

 end;

 theorem :: BORSUK_5:55



 Th54: for A be Subset of R^1 , a,b be Real st a < b & A = ( ].a, b.[ \/ ].b, +infty .[) holds ( Cl A) = [.a, +infty .[

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ( ].a, b.[ \/ ].b, +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 Th48;

 ( Cl B) = [.a, b.] by A1, Th15;

 hence thesis by A1, A3, A4, Th10;

 end;

 theorem :: BORSUK_5:56

 for A be Subset of R^1 , a,b,c be Real 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 ;

 let a,b,c be Real;

 assume that

 A1: a < b and

 A2: b < c;

 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 .[);

 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, Th54;

 then ( Cl A) = ( [.a, b.] \/ [.b, +infty .[) by A1, Th30;

 hence thesis by A1, Th10;

 end;

 theorem :: BORSUK_5:57



 Th56: for a,b be Real holds ( IRRAT (a,b)) misses ( RAT (a,b))

 proof

 let a,b be Real;

 assume ( IRRAT (a,b)) meets ( RAT (a,b));

 then

 consider x be object such that

 A1: x in ( IRRAT (a,b)) and

 A2: x in ( RAT (a,b)) by XBOOLE_0: 3;

 thus thesis by A1, A2, Th29;

 end;

 theorem :: BORSUK_5:58



 Th57: for a,b be Real holds ( REAL \ ( RAT (a,b))) = (( ]. -infty , a.] \/ ( IRRAT (a,b))) \/ [.b, +infty .[)

 proof

 let a,b be Real;

 thus ( REAL \ ( RAT (a,b))) c= (( ]. -infty , a.] \/ ( IRRAT (a,b))) \/ [.b, +infty .[)

 proof

 let x be object;

 assume

 A1: x in ( REAL \ ( RAT (a,b)));

 then

 A2: not x in ( RAT (a,b)) by XBOOLE_0:def 5;

 reconsider x as Real by A1;

 per cases ;

 suppose x <= a & x < b;

 then x in ]. -infty , a.] by XXREAL_1: 234;

 then x in ( ]. -infty , a.] \/ ( IRRAT (a,b))) by XBOOLE_0:def 3;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose x <= a & x >= b;

 then x in ]. -infty , a.] by XXREAL_1: 234;

 then x in ( ]. -infty , a.] \/ ( IRRAT (a,b))) by XBOOLE_0:def 3;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose

 A3: x > a & x < b;

 x in ( IRRAT (a,b))

 proof

 per cases ;

 suppose x is rational;

 hence thesis by A2, A3, Th28;

 end;

 suppose x is irrational;

 hence thesis by A3, Th29;

 end;

 end;

 then x in ( ]. -infty , a.] \/ ( IRRAT (a,b))) by XBOOLE_0:def 3;

 hence thesis by XBOOLE_0:def 3;

 end;

 suppose x > a & x >= b;

 then x in [.b, +infty .[ by XXREAL_1: 236;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 let x be object;

 assume

 A4: x in (( ]. -infty , a.] \/ ( IRRAT (a,b))) \/ [.b, +infty .[);

 then

 reconsider x as Real;



 A5: x in ( ]. -infty , a.] \/ ( IRRAT (a,b))) or x in [.b, +infty .[ by A4, XBOOLE_0:def 3;

 per cases by A5, XBOOLE_0:def 3;

 suppose x in ]. -infty , a.];

 then x <= a by XXREAL_1: 234;

 then

 A6: not x in ( RAT (a,b)) by Th28;

 x in REAL by XREAL_0:def 1;

 hence thesis by A6, XBOOLE_0:def 5;

 end;

 suppose

 A7: x in ( IRRAT (a,b));

 ( IRRAT (a,b)) misses ( RAT (a,b)) by Th56;

 then

 A8: not x in ( RAT (a,b)) by A7, XBOOLE_0: 3;

 x in REAL by XREAL_0:def 1;

 hence thesis by A8, XBOOLE_0:def 5;

 end;

 suppose x in [.b, +infty .[;

 then x >= b by XXREAL_1: 236;

 then

 A9: not x in ( RAT (a,b)) by Th28;

 x in REAL by XREAL_0:def 1;

 hence thesis by A9, XBOOLE_0:def 5;

 end;

 end;

 theorem :: BORSUK_5:59



 Th58: for a,b be Real st a < b holds ( [.a, +infty .[ \ ( ].a, b.[ \/ ].b, +infty .[)) = ( {a} \/ {b})

 proof

 let a,b be Real;



 A1: not b in ( ].a, b.[ \/ ].b, +infty .[) by XXREAL_1: 205;

 assume

 A2: a < b;

 then

 A3: not a in ( ].a, b.[ \/ ].b, +infty .[) by XXREAL_1: 223;

 [.a, +infty .[ = ( [.a, b.] \/ [.b, +infty .[) by A2, Th10

 .= (( {a, b} \/ ].a, b.[) \/ [.b, +infty .[) by A2, XXREAL_1: 128

 .= (( {a, b} \/ ].a, b.[) \/ ( {b} \/ ].b, +infty .[)) by Th42

 .= ((( {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 thesis by ENUMSET1: 1;

 end;

 theorem :: BORSUK_5:60

 for A be 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 object;

 assume

 A2: x in ( ]. -infty , 2.] \/ ( IRRAT (2,4)));

 then

 reconsider x as Real;

 per cases by A2, XBOOLE_0:def 3;

 suppose x in ]. -infty , 2.];

 then x <= 2 by XXREAL_1: 234;

 then x <= 4 by XXREAL_0: 2;

 hence thesis by XXREAL_1: 234;

 end;

 suppose x in ( IRRAT (2,4));

 then x < 4 by Th29;

 hence thesis by XXREAL_1: 234;

 end;

 end;

 let A be Subset of R^1 ;



 A3: ( ].4, 5.[ \/ ].5, +infty .[) c= ].4, +infty .[

 proof

 let x be object;

 assume

 A4: x in ( ].4, 5.[ \/ ].5, +infty .[);

 then

 reconsider x as Real;

 per cases by A4, XBOOLE_0:def 3;

 suppose x in ].4, 5.[;

 then x > 4 by XXREAL_1: 4;

 hence thesis by XXREAL_1: 235;

 end;

 suppose x in ].5, +infty .[;

 then x > 5 by XXREAL_1: 235;

 then x > 4 by XXREAL_0: 2;

 hence thesis by XXREAL_1: 235;

 end;

 end;

 assume A = ((( RAT (2,4)) \/ ].4, 5.[) \/ ].5, +infty .[);



 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 Th57;

 ]. -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 Th58

 .= ((( ]. -infty , 2.] \/ ( IRRAT (2,4))) \/ {4}) \/ {5}) by XBOOLE_1: 4;

 hence thesis;

 end;

 theorem :: BORSUK_5:61

 for A be Subset of R^1 , a be Real 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 object;

 assume

 A1: x in ((( IRRAT (2,4)) \/ {4}) \/ {5});

 then

 reconsider x as Real;



 A2: x in (( IRRAT (2,4)) \/ {4}) or x in {5} by A1, XBOOLE_0:def 3;

 per cases by A2, XBOOLE_0:def 3;

 suppose x in ( IRRAT (2,4));

 then x > 2 by Th29;

 then x > 1 by XXREAL_0: 2;

 hence thesis by XXREAL_1: 235;

 end;

 suppose x in {4};

 then x = 4 by TARSKI:def 1;

 hence thesis by XXREAL_1: 235;

 end;

 suppose x in {5};

 then x = 5 by TARSKI:def 1;

 hence thesis by XXREAL_1: 235;

 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 object;

 assume

 A2: x in ]. -infty , 1.[;

 then

 reconsider x as Real;

 x < 1 by A2, XXREAL_1: 233;

 then x < 2 by XXREAL_0: 2;

 hence thesis by XXREAL_1: 234;

 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 thesis;

 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 thesis;

 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 thesis by XBOOLE_1: 4;

 end;

 theorem :: BORSUK_5:63

 for A be Subset of R^1 , a,b be Real st a <= b & A = ( {a} \/ [.b, +infty .[) holds (A ` ) = ( ]. -infty , a.[ \/ ].a, b.[)

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a <= b and

 A2: A = ( {a} \/ [.b, +infty .[);

 (A ` ) = (( REAL \ [.b, +infty .[) \ {a}) by A2, TOPMETR: 17, XBOOLE_1: 41

 .= ( ]. -infty , b.[ \ {a}) by XXREAL_1: 224, XXREAL_1: 294;

 hence thesis by A1, XXREAL_1: 349;

 end;

 theorem :: BORSUK_5:64

 for A be Subset of R^1 , a,b be Real st a < b & A = ( ]. -infty , a.[ \/ ].a, b.[) holds ( Cl A) = ]. -infty , b.]

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ( ]. -infty , a.[ \/ ].a, b.[);

 reconsider B = ]. -infty , a.[, C = ].a, b.[ as Subset of R^1 by TOPMETR: 17;



 A3: ( Cl C) = [.a, b.] by A1, Th15;

 ( Cl A) = (( Cl B) \/ ( Cl C)) by A2, PRE_TOPC: 20

 .= ( ]. -infty , a.] \/ [.a, b.]) by A3, Th50

 .= ]. -infty , b.] by A1, Th11;

 hence thesis;

 end;

 theorem :: BORSUK_5:65



 Th64: for A be Subset of R^1 , a,b be Real st a < b & A = ( ]. -infty , a.[ \/ ].a, b.]) holds ( Cl A) = ]. -infty , b.]

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a < b and

 A2: A = ( ]. -infty , a.[ \/ ].a, b.]);

 reconsider B = ]. -infty , a.[, C = ].a, b.] as Subset of R^1 by TOPMETR: 17;



 A3: ( Cl C) = [.a, b.] by A1, Th35;

 ( Cl A) = (( Cl B) \/ ( Cl C)) by A2, PRE_TOPC: 20

 .= ( ]. -infty , a.] \/ [.a, b.]) by A3, Th50

 .= ]. -infty , b.] by A1, Th11;

 hence thesis;

 end;

 theorem :: BORSUK_5:66



 Th65: for A be Subset of R^1 , a,b,c be Real 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 , a,b,c be Real;

 assume that

 A1: a < b and

 A2: b < c and

 A3: A = ((( ]. -infty , a.[ \/ ].a, b.]) \/ ( IRRAT (b,c))) \/ {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 Th37

 .= ((( Cl (B \/ C)) \/ ( Cl D)) \/ E) by PRE_TOPC: 20

 .= (( ]. -infty , b.] \/ ( Cl D)) \/ E) by A1, Th64

 .= (( ]. -infty , b.] \/ [.b, c.]) \/ E) by A2, Th31

 .= ( ]. -infty , c.] \/ E) by A2, Th11

 .= ]. -infty , c.] by A4, ZFMISC_1: 40;

 hence thesis;

 end;

 theorem :: BORSUK_5:67

 for A be Subset of R^1 , a,b,c,d be Real 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 , a,b,c,d be Real;

 assume that

 A1: a < b and

 A2: b < c and

 A3: A = (((( ]. -infty , a.[ \/ ].a, b.]) \/ ( IRRAT (b,c))) \/ {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 Th37;

 hence thesis by A1, A2, Th65;

 end;

 theorem :: BORSUK_5:68

 for A be Subset of R^1 , a,b be Real st a <= b & A = ( ]. -infty , a.] \/ {b}) holds (A ` ) = ( ].a, b.[ \/ ].b, +infty .[)

 proof

 let A be Subset of R^1 , a,b be Real;

 assume that

 A1: a <= b and

 A2: A = ( ]. -infty , a.] \/ {b});

 (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 thesis;

 end;

 theorem :: BORSUK_5:69

 for a,b be Real holds ( [.a, +infty .[ \/ {b}) <> REAL

 proof

 let a,b be Real;

 set ab = (( min (a,b)) - 1);



 A1: ab < ( min (a,b)) by XREAL_1: 146;

 ( min (a,b)) <= b by XXREAL_0: 17;

 then

 A2: not ab in {b} by A1, TARSKI:def 1;

 ( min (a,b)) <= a by XXREAL_0: 17;

 then ab < a by XREAL_1: 146, XXREAL_0: 2;

 then

 A3: not ab in [.a, +infty .[ by XXREAL_1: 236;

 ab in REAL by XREAL_0:def 1;

 hence thesis by A3, A2, XBOOLE_0:def 3;

 end;

 theorem :: BORSUK_5:70

 for a,b be Real holds ( ]. -infty , a.] \/ {b}) <> REAL

 proof

 let a,b be Real;

 set ab = (( max (a,b)) + 1);



 A1: ab > ( max (a,b)) by XREAL_1: 29;

 ( max (a,b)) >= a by XXREAL_0: 25;

 then ab > a by A1, XXREAL_0: 2;

 then

 A2: not ab in ]. -infty , a.] by XXREAL_1: 234;

 ( max (a,b)) >= b by XXREAL_0: 25;

 then

 A3: not ab in {b} by A1, TARSKI:def 1;

 ab in REAL by XREAL_0:def 1;

 hence thesis by A2, A3, XBOOLE_0:def 3;

 end;

 theorem :: BORSUK_5:71

 for TS be TopStruct, A,B be Subset of TS st A <> B holds (A ` ) <> (B ` )

 proof

 let TS be TopStruct, A,B be Subset of TS;

 assume

 A1: A <> B;

 assume (A ` ) = (B ` );

 then A = ((B ` ) ` );

 hence thesis by A1;

 end;

 theorem :: BORSUK_5:72

 for A be 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 ;

 assume REAL = (A ` );

 then (AB ` ) = (A ` ) by TOPMETR: 17;

 then AB = ((A ` ) ` );

 hence thesis;

 end;

 begin

 theorem :: BORSUK_5:73



 Th72: for X be compact Subset of R^1 , X9 be Subset of REAL st X9 = X holds X9 is bounded_above bounded_below

 proof

 let X be compact Subset of R^1 , X9 be Subset of REAL ;

 assume X9 = X;

 then X9 is compact by JORDAN5A: 25;

 then X9 is real-bounded by RCOMP_1: 10;

 hence thesis by XXREAL_2:def 11;

 end;

 theorem :: BORSUK_5:74



 Th73: for X be compact Subset of R^1 , X9 be Subset of REAL , x be Real st x in X9 & X9 = X holds ( lower_bound X9) <= x & x <= ( upper_bound X9)

 proof

 let X be compact Subset of R^1 , X9 be Subset of REAL , x be Real;

 assume that

 A1: x in X9 and

 A2: X9 = X;

 X9 is bounded_above bounded_below by A2, Th72;

 hence thesis by A1, SEQ_4:def 1, SEQ_4:def 2;

 end;

 theorem :: BORSUK_5:75



 Th74: for C be non empty compact connected Subset of R^1 , C9 be 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 compact connected Subset of R^1 , C9 be Subset of REAL ;

 assume that

 A1: C = C9 and

 A2: [.( lower_bound C9), ( upper_bound C9).] c= C9;

 assume [.( lower_bound C9), ( upper_bound C9).] <> C9;

 then not C9 c= [.( lower_bound C9), ( upper_bound C9).] by A2, XBOOLE_0:def 10;

 then

 consider c be object such that

 A3: c in C9 and

 A4: not c in [.( lower_bound C9), ( upper_bound C9).];

 reconsider c as Real by A3;



 A5: c <= ( upper_bound C9) by A1, A3, Th73;

 ( lower_bound C9) <= c by A1, A3, Th73;

 hence thesis by A4, A5, XXREAL_1: 1;

 end;

 theorem :: BORSUK_5:76



 Th75: for A be connected Subset of R^1 , a,b,c be Real st a <= b & b <= c & a in A & c in A holds b in A

 proof

 let A be connected Subset of R^1 , a,b,c be Real;

 assume that

 A1: a <= b and

 A2: b <= c and

 A3: a in A and

 A4: c in A;

 per cases by A1, A2, A3, A4, XXREAL_0: 1;

 suppose a = b or b = c;

 hence thesis by A3, A4;

 end;

 suppose

 A5: a < b & b < c & a in A & c in A;

 reconsider B = ]. -infty , b.[, C = ].b, +infty .[ as Subset of R^1 by TOPMETR: 17;

 assume not b in A;

 then A c= ( REAL \ {b}) by TOPMETR: 17, ZFMISC_1: 34;

 then

 A6: A c= ( ]. -infty , b.[ \/ ].b, +infty .[) by XXREAL_1: 389;

 now

 per cases by A6, Th52, CONNSP_1: 16;

 suppose A c= B;

 hence contradiction by A5, XXREAL_1: 233;

 end;

 suppose A c= C;

 hence contradiction by A5, XXREAL_1: 235;

 end;

 end;

 hence thesis;

 end;

 end;

 theorem :: BORSUK_5:77



 Th76: for A be connected Subset of R^1 , a,b be Real st a in A & b in A holds [.a, b.] c= A

 proof

 let A be connected Subset of R^1 , a,b be Real;

 assume that

 A1: a in A and

 A2: b in A;

 let x be object;

 assume x in [.a, b.];

 then x in { y where y be Real : a <= y & y <= b } by RCOMP_1:def 1;

 then ex z be Real st z = x & a <= z & z <= b;

 hence thesis by A1, A2, Th75;

 end;

 theorem :: BORSUK_5:78



 Th77: for X be non empty compact connected Subset of R^1 holds X is non empty non empty closed_interval Subset of REAL

 proof

 let C be non empty compact connected Subset of R^1 ;

 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 Th72, RCOMP_1: 12;

 C9 is bounded_below bounded_above by Th72;

 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, Th72, RCOMP_1: 13;

 then [.( lower_bound C9), ( upper_bound C9).] = C9 by A2, Th74, Th76;

 then C9 is non empty closed_interval by A3, MEASURE5: 14;

 hence thesis;

 end;

 theorem :: BORSUK_5:79

 for A be non empty compact connected Subset of R^1 holds ex a,b be Real st a <= b & A = [.a, b.]

 proof

 let C be non empty compact connected Subset of R^1 ;

 reconsider C9 = C as non empty closed_interval Subset of REAL by Th77;



 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, p2;

 thus p1 <= p2 by BORSUK_4: 28;

 thus thesis by INTEGRA1: 4;

 end;

 registration

 let T be TopSpace;

 cluster open closed non empty for Subset-Family of T;

 existence

 proof

 reconsider F = {( {} T)} as Subset-Family of T by ZFMISC_1: 31;



 A1: F is closed by TARSKI:def 1;

 F is open by TARSKI:def 1;

 hence thesis by A1;

 end;

 end