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