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 ) by ;
A2: ( b in REAL or b in ) by ;
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 ;
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 ;
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 ;
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 ; :: 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 ; :: 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;