let A be Subset of R^1; :: thesis: for a, b, c being Real st A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c holds

Int A = ].-infty,a.[

let a, b, c be Real; :: thesis: ( A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c implies Int A = ].-infty,a.[ )

reconsider B = [.a,b.], C = IRRAT (b,c), D = [.c,+infty.[ as Subset of R^1 by TOPMETR:17;

assume that

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

A2: a < b and

A3: b < c ; :: thesis: Int A = ].-infty,a.[

A4: a < c by A2, A3, XXREAL_0:2;

A ` = REAL \ (].-infty,a.[ \/ (RAT (b,c))) by A1, TOPMETR:17

.= (REAL \ (RAT (b,c))) \ ].-infty,a.[ by XBOOLE_1:41

.= ((].-infty,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[) \ ].-infty,a.[ by BORSUK_5:58

.= (].-infty,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[)) \ ].-infty,a.[ by XBOOLE_1:4

.= (].-infty,b.] \ ].-infty,a.[) \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XBOOLE_1:42 ;

then A5: A ` = [.a,b.] \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XXREAL_1:289

.= [.a,b.] \/ (((IRRAT (b,c)) \ ].-infty,a.[) \/ ([.c,+infty.[ \ ].-infty,a.[)) by XBOOLE_1:42 ;

right_closed_halfline c is closed ;

then D is closed by JORDAN5A:23;

then A6: Cl D = D by PRE_TOPC:22;

[.b,+infty.[ misses ].-infty,a.[ by A2, XXREAL_1:94;

then IRRAT (b,c) misses ].-infty,a.[ by Th31, XBOOLE_1:63;

then A7: (IRRAT (b,c)) \ ].-infty,a.[ = IRRAT (b,c) by XBOOLE_1:83;

B is closed by JORDAN5A:23;

then A8: Cl B = B by PRE_TOPC:22;

[.c,+infty.[ misses ].-infty,a.[ by A2, A3, XXREAL_0:2, XXREAL_1:94;

then A ` = [.a,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[) by A5, A7, XBOOLE_1:83

.= [.a,b.] \/ ((IRRAT (b,c)) \/ ({c} \/ ].c,+infty.[)) by BORSUK_5:43

.= ([.a,b.] \/ (IRRAT (b,c))) \/ ({c} \/ ].c,+infty.[) by XBOOLE_1:4

.= ([.a,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[ by BORSUK_5:43 ;

then Cl (A `) = (Cl (B \/ C)) \/ (Cl D) by PRE_TOPC:20

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

.= (B \/ [.b,c.]) \/ D by A8, A6, A3, BORSUK_5:32

.= [.a,c.] \/ D by A2, A3, XXREAL_1:165

.= [.a,+infty.[ by A4, BORSUK_5:11 ;

then (Cl (A `)) ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294;

hence Int A = ].-infty,a.[ by TOPS_1:def 1; :: thesis: verum

Int A = ].-infty,a.[

let a, b, c be Real; :: thesis: ( A = ].-infty,a.[ \/ (RAT (b,c)) & a < b & b < c implies Int A = ].-infty,a.[ )

reconsider B = [.a,b.], C = IRRAT (b,c), D = [.c,+infty.[ as Subset of R^1 by TOPMETR:17;

assume that

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

A2: a < b and

A3: b < c ; :: thesis: Int A = ].-infty,a.[

A4: a < c by A2, A3, XXREAL_0:2;

A ` = REAL \ (].-infty,a.[ \/ (RAT (b,c))) by A1, TOPMETR:17

.= (REAL \ (RAT (b,c))) \ ].-infty,a.[ by XBOOLE_1:41

.= ((].-infty,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[) \ ].-infty,a.[ by BORSUK_5:58

.= (].-infty,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[)) \ ].-infty,a.[ by XBOOLE_1:4

.= (].-infty,b.] \ ].-infty,a.[) \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XBOOLE_1:42 ;

then A5: A ` = [.a,b.] \/ (((IRRAT (b,c)) \/ [.c,+infty.[) \ ].-infty,a.[) by XXREAL_1:289

.= [.a,b.] \/ (((IRRAT (b,c)) \ ].-infty,a.[) \/ ([.c,+infty.[ \ ].-infty,a.[)) by XBOOLE_1:42 ;

right_closed_halfline c is closed ;

then D is closed by JORDAN5A:23;

then A6: Cl D = D by PRE_TOPC:22;

[.b,+infty.[ misses ].-infty,a.[ by A2, XXREAL_1:94;

then IRRAT (b,c) misses ].-infty,a.[ by Th31, XBOOLE_1:63;

then A7: (IRRAT (b,c)) \ ].-infty,a.[ = IRRAT (b,c) by XBOOLE_1:83;

B is closed by JORDAN5A:23;

then A8: Cl B = B by PRE_TOPC:22;

[.c,+infty.[ misses ].-infty,a.[ by A2, A3, XXREAL_0:2, XXREAL_1:94;

then A ` = [.a,b.] \/ ((IRRAT (b,c)) \/ [.c,+infty.[) by A5, A7, XBOOLE_1:83

.= [.a,b.] \/ ((IRRAT (b,c)) \/ ({c} \/ ].c,+infty.[)) by BORSUK_5:43

.= ([.a,b.] \/ (IRRAT (b,c))) \/ ({c} \/ ].c,+infty.[) by XBOOLE_1:4

.= ([.a,b.] \/ (IRRAT (b,c))) \/ [.c,+infty.[ by BORSUK_5:43 ;

then Cl (A `) = (Cl (B \/ C)) \/ (Cl D) by PRE_TOPC:20

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

.= (B \/ [.b,c.]) \/ D by A8, A6, A3, BORSUK_5:32

.= [.a,c.] \/ D by A2, A3, XXREAL_1:165

.= [.a,+infty.[ by A4, BORSUK_5:11 ;

then (Cl (A `)) ` = ].-infty,a.[ by TOPMETR:17, XXREAL_1:224, XXREAL_1:294;

hence Int A = ].-infty,a.[ by TOPS_1:def 1; :: thesis: verum