let a, b be R_eal; :: thesis: ( a < b implies ex c being Real st
( a < c & c < b ) )
assume A1: a < b ; :: thesis: ex c being Real st
( a < c & c < b )

per cases ( a in REAL or b in REAL or ( not a in REAL & not b in REAL ) ) ;

suppose A2: a in REAL ; :: thesis: ex c being Real st
( a < c & c < b )

then A3: ( b in REAL or b = +infty ) by A1, XXREAL_0:10;

now :: thesis: ( b = +infty implies ex c being Real st
( a < c & c < b ) )

assume A4: b = +infty ; :: thesis: ex c being Real st
( a < c & c < b )
consider c being Real such that
A5: a < c by A2, XREAL_1:1;
c in REAL by XREAL_0:def 1;
hence ex c being Real st
( a < c & c < b ) by A5, A4, XXREAL_0:9; :: thesis: verum

end;

hence ex c being Real st
( a < c & c < b ) by A3, A1, A2, XREAL_1:5; :: thesis: verum

end;

suppose A6: b in REAL ; :: thesis: ex c being Real st
( a < c & c < b )

then A7: ( a in REAL or a = -infty ) by A1, XXREAL_0:13;

now :: thesis: ( a = -infty implies ex c being Real st
( a < c & c < b ) )

assume A8: a = -infty ; :: thesis: ex c being Real st
( a < c & c < b )
consider c being Real such that
A9: c < b by A6, XREAL_1:2;
c in REAL by XREAL_0:def 1;
hence ex c being Real st
( a < c & c < b ) by A9, A8, XXREAL_0:12; :: thesis: verum

end;

hence ex c being Real st
( a < c & c < b ) by A7, A1, A6, XREAL_1:5; :: thesis: verum

end;

suppose ( not a in REAL & not b in REAL ) ; :: thesis: ex c being Real st
( a < c & c < b )

then ( a = +infty or ( a = -infty & b = +infty ) or b = -infty ) by XXREAL_0:14;
then ( a < 0 & 0 < b ) by A1, XXREAL_0:4, XXREAL_0:6;
hence ex c being Real st
( a < c & c < b ) ; :: thesis: verum

end;

end;