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;

( 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;

end;

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

( a < x & x < b & x in REAL )

( 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;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

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

( a < x & x < b & x in REAL )

( 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;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

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

( a < x & x < b & x in REAL )

( 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;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