let a, b be Real; :: thesis: ( a in REAL \ ].a,b.[ & b in REAL \ ].a,b.[ )
( a <= a & -infty < a ) by XXREAL_0:12, XREAL_0:def 1;
then a in ].-infty,a.] ;
then a in ].-infty,a.] \/ [.b,+infty.[ by XBOOLE_0:def 3;
hence a in REAL \ ].a,b.[ by XXREAL_1:398; :: thesis: b in REAL \ ].a,b.[
( b <= b & b < +infty ) by XXREAL_0:9, XREAL_0:def 1;
then b in [.b,+infty.[ ;
then b in ].-infty,a.] \/ [.b,+infty.[ by XBOOLE_0:def 3;
hence b in REAL \ ].a,b.[ by XXREAL_1:398; :: thesis: verum