let A be Subset of R^1 ; :: thesis: for a, b, c being real number st A = ].-infty ,a.[ \/ (RAT b,c) & a < b & b < c holds
Int A = ].-infty ,a.[
let a, b, c be real number ; :: 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:24;
B is closed by TOPREAL6:79;
then A1: Cl B = B by PRE_TOPC:52;
right_closed_halfline c is closed ;
then D is closed by TOPREAL6:79;
then A2: Cl D = D by PRE_TOPC:52;
assume A3: ( A = ].-infty ,a.[ \/ (RAT b,c) & a < b & b < c ) ; :: thesis: Int A = ].-infty ,a.[
then A ` = REAL \ (].-infty ,a.[ \/ (RAT b,c)) by TOPMETR:24
.= (REAL \ (RAT b,c)) \ ].-infty ,a.[ by XBOOLE_1:41
.= ((].-infty ,b.] \/ (IRRAT b,c)) \/ [.c,+infty .[) \ ].-infty ,a.[ by BORSUK_5:85
.= (].-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 A4: 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 ;
IRRAT b,c misses ].-infty ,a.[

proof

[.b,+infty .[ misses ].-infty ,a.[ by A3, XXREAL_1:94;
hence IRRAT b,c misses ].-infty ,a.[ by Th36, XBOOLE_1:63; :: thesis: verum

end;

then A5: (IRRAT b,c) \ ].-infty ,a.[ = IRRAT b,c by XBOOLE_1:83;
A6: a < c by A3, XXREAL_0:2;
[.c,+infty .[ misses ].-infty ,a.[ by A3, XXREAL_0:2, XXREAL_1:94;
then A ` = [.a,b.] \/ ((IRRAT b,c) \/ [.c,+infty .[) by A4, A5, XBOOLE_1:83
.= [.a,b.] \/ ((IRRAT b,c) \/ ({c} \/ ].c,+infty .[)) by BORSUK_5:67
.= ([.a,b.] \/ (IRRAT b,c)) \/ ({c} \/ ].c,+infty .[) by XBOOLE_1:4
.= ([.a,b.] \/ (IRRAT b,c)) \/ [.c,+infty .[ by BORSUK_5:67 ;
then Cl (A ` ) = (Cl (B \/ C)) \/ (Cl D) by PRE_TOPC:50
.= ((Cl B) \/ (Cl C)) \/ (Cl D) by PRE_TOPC:50
.= (B \/ [.b,c.]) \/ D by A1, A2, A3, BORSUK_5:55
.= [.a,c.] \/ D by A3, XXREAL_1:165
.= [.a,+infty .[ by A6, BORSUK_5:28 ;
then (Cl (A ` )) ` = ].-infty ,a.[ by TOPMETR:24, XXREAL_1:224, XXREAL_1:294;
hence Int A = ].-infty ,a.[ by TOPS_1:def 1; :: thesis: verum