let a, b be R_eal; :: thesis: ( a < b implies ex x being R_eal st
( a < x & x < b & x in REAL ) )
A1: ( a in REAL or a in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;
A2: ( b in REAL or b in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;
assume A3: a < b ; :: thesis: ex x being R_eal st
( a < x & x < b & x in REAL )
then A4: ( not a = +infty & not b = -infty ) by XXREAL_0:4, XXREAL_0:6;

per cases ( ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) ) by A1, A2, A4, TARSKI:def 2;

suppose ( a in REAL & b in REAL ) ; :: thesis: ex x being R_eal st
( a < x & x < b & x in REAL )

then consider x, y being Real such that
A5: ( x = a & y = b ) and
x <= y by A3;
consider z being Real such that
A6: ( x < z & z < y ) by A3, A5, XREAL_1:5;
reconsider z = z as Element of REAL by XREAL_0:def 1;
reconsider o = z as R_eal by XXREAL_0:def 1;
take o ; :: thesis: ( a < o & o < b & o in REAL )
thus ( a < o & o < b & o in REAL ) by A5, A6; :: thesis: verum

end;

suppose A7: ( a in REAL & b = +infty ) ; :: thesis: ex x being R_eal st
( a < x & x < b & x in REAL )

then reconsider x = a as Real ;
consider z being Real such that
A8: x < z by XREAL_1:1;
reconsider z = z as Element of REAL by XREAL_0:def 1;
reconsider o = z as R_eal by XXREAL_0:def 1;
take o ; :: thesis: ( a < o & o < b & o in REAL )
thus ( a < o & o < b & o in REAL ) by A7, A8, XXREAL_0:9; :: thesis: verum

end;

suppose A9: ( a = -infty & b in REAL ) ; :: thesis: ex x being R_eal st
( a < x & x < b & x in REAL )

then reconsider y = b as Real ;
consider z being Real such that
A10: z < y by XREAL_1:2;
reconsider z = z as Element of REAL by XREAL_0:def 1;
reconsider o = z as R_eal by XXREAL_0:def 1;
take o ; :: thesis: ( a < o & o < b & o in REAL )
thus ( a < o & o < b & o in REAL ) by A9, A10, XXREAL_0:12; :: thesis: verum

end;

suppose A11: ( a = -infty & b = +infty ) ; :: thesis: ex x being R_eal st
( a < x & x < b & x in REAL )

take 0. ; :: thesis: ( a < 0. & 0. < b & 0. in REAL )
0. = In (0,REAL) ;
hence ( a < 0. & 0. < b & 0. in REAL ) by A11; :: thesis: verum

end;

end;