let a, b be real number ; :: 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:67
.= ].-infty ,a.[ \/ ([.a,b.] \/ [.b,+infty .[) by A1, BORSUK_5:28
.= ].-infty ,a.[ \/ ([.a,b.] \/ ({b} \/ ].b,+infty .[)) by BORSUK_5:67
.= ].-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