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;
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: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 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 TOPREAL6:79;
then A6: Cl D = D by PRE_TOPC:52;
[.b,+infty .[ misses ].-infty ,a.[ by A2, XXREAL_1:94;
then IRRAT b,c misses ].-infty ,a.[ by Th36, XBOOLE_1:63;
then A7: (IRRAT b,c) \ ].-infty ,a.[ = IRRAT b,c by XBOOLE_1:83;
B is closed by TOPREAL6:79;
then A8: Cl B = B by PRE_TOPC:52;
[.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: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 A8, A6, A3, BORSUK_5:55
.= [.a,c.] \/ D by A2, A3, XXREAL_1:165
.= [.a,+infty .[ by A4, 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