let A be Subset of R^1; :: thesis: for a, b, c being Real st A = ].-infty,a.] \/ [.b,c.] & a < b & b < c holds
Int A = ].-infty,a.[ \/ ].b,c.[
let a, b, c be Real; :: 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:17;
A5: Cl B = [.a,b.] by A2, BORSUK_5:16;
A6: Cl C = [.c,+infty.[ by BORSUK_5:49;
A ` = REAL \ (].-infty,a.] \/ [.b,c.]) by A1, TOPMETR:17
.= (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:20, TOPMETR:17
.= (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