let a, b be Real; :: thesis: ( a < b implies REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ )
assume A1: a < b ; :: thesis: REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[
REAL = (REAL \ {a}) \/ {a} by XBOOLE_1:45
.= (].-infty,a.[ \/ ].a,+infty.[) \/ {a} by XXREAL_1:389
.= ].-infty,a.[ \/ (].a,+infty.[ \/ {a}) by XBOOLE_1:4
.= ].-infty,a.[ \/ [.a,+infty.[ by BORSUK_5:43
.= ].-infty,a.[ \/ ([.a,b.] \/ [.b,+infty.[) by A1, BORSUK_5:11
.= ].-infty,a.[ \/ ([.a,b.] \/ ({b} \/ ].b,+infty.[)) by BORSUK_5:43
.= ].-infty,a.[ \/ (([.a,b.] \/ {b}) \/ ].b,+infty.[) by XBOOLE_1:4
.= (].-infty,a.[ \/ ([.a,b.] \/ {b})) \/ ].b,+infty.[ by XBOOLE_1:4 ;
hence REAL = (].-infty,a.[ \/ [.a,b.]) \/ ].b,+infty.[ by A1, Lm1; :: thesis: verum