let A be Subset of R^1 ; :: thesis: for a, b, c being real number st A = ].-infty ,a.] \/ [.b,c.] & a < b & b < c holds
Int A = ].-infty ,a.[ \/ ].b,c.[
let a, b, c be real number ; :: thesis: ( A = ].-infty ,a.] \/ [.b,c.] & a < b & b < c implies Int A = ].-infty ,a.[ \/ ].b,c.[ )
assume that
A1: A = ].-infty ,a.] \/ [.b,c.] and
A2: a < b and
A3: b < c ; :: thesis: Int A = ].-infty ,a.[ \/ ].b,c.[
a < c by A2, A3, XXREAL_0:2;
then A4: ].c,+infty .[ /\ ].a,+infty .[ = ].c,+infty .[ by XBOOLE_1:28, XXREAL_1:46;
reconsider B = ].a,b.[, C = ].c,+infty .[ as Subset of R^1 by TOPMETR:24;
A5: Cl B = [.a,b.] by A2, BORSUK_5:36;
A6: Cl C = [.c,+infty .[ by BORSUK_5:75;
A ` = REAL \ (].-infty ,a.] \/ [.b,c.]) by A1, TOPMETR:24
.= (REAL \ (left_closed_halfline a)) \ [.b,c.] by XBOOLE_1:41
.= (right_open_halfline a) \ [.b,c.] by XXREAL_1:224, XXREAL_1:288
.= ].a,+infty .[ \ ([.b,+infty .[ \ ].c,+infty .[) by XXREAL_1:295
.= (].a,+infty .[ \ [.b,+infty .[) \/ (].a,+infty .[ /\ ].c,+infty .[) by XBOOLE_1:52
.= ].a,b.[ \/ ].c,+infty .[ by A4, XXREAL_1:294 ;
then (Cl (A ` )) ` = REAL \ ([.c,+infty .[ \/ [.a,b.]) by A5, A6, PRE_TOPC:50, TOPMETR:24
.= (REAL \ (right_closed_halfline c)) \ [.a,b.] by XBOOLE_1:41
.= (left_open_halfline c) \ [.a,b.] by XXREAL_1:224, XXREAL_1:294
.= ].-infty ,a.[ \/ ].b,c.[ by A2, A3, XXREAL_0:2, XXREAL_1:339 ;
hence Int A = ].-infty ,a.[ \/ ].b,c.[ by TOPS_1:def 1; :: thesis: verum