let r, t be ExtReal; :: thesis: ( r < t implies ex s being ExtReal st
( r < s & s < t ) )
assume A1: r < t ; :: thesis: ex s being ExtReal st
( r < s & s < t )
then A2: r <> +infty by XXREAL_0:3;
A3: t <> -infty by A1, XXREAL_0:5;

per cases ( ( r = -infty & t = +infty ) or ( r = -infty & t in REAL ) or ( r in REAL & t = +infty ) or ( r in REAL & t in REAL ) ) by A2, A3, XXREAL_0:14;

suppose that A4: r = -infty and
A5: t = +infty ; :: thesis: ex s being ExtReal st
( r < s & s < t )

take 0 ; :: thesis: ( r < 0 & 0 < t )
thus ( r < 0 & 0 < t ) by A4, A5; :: thesis: verum

end;

suppose that A6: r = -infty and
A7: t in REAL ; :: thesis: ex s being ExtReal st
( r < s & s < t )

reconsider t = t as Real by A7;
consider s being Real such that
A8: s < t by Th2;
take s ; :: thesis: ( r < s & s < t )
s in REAL by XREAL_0:def 1;
hence r < s by A6, XXREAL_0:12; :: thesis: s < t
thus s < t by A8; :: thesis: verum

end;

suppose that A9: r in REAL and
A10: t = +infty ; :: thesis: ex s being ExtReal st
( r < s & s < t )

reconsider r9 = r as Real by A9;
consider s being Real such that
A11: r9 < s by Th1;
take s ; :: thesis: ( r < s & s < t )
thus r < s by A11; :: thesis: s < t
s in REAL by XREAL_0:def 1;
hence s < t by A10, XXREAL_0:9; :: thesis: verum

end;

suppose that A12: r in REAL and
A13: t in REAL ; :: thesis: ex s being ExtReal st
( r < s & s < t )

reconsider r = r, t = t as Real by A12, A13;
consider s being Real such that
A14: ( r < s & s < t ) by A1, Th5;
take s ; :: thesis: ( r < s & s < t )
thus ( r < s & s < t ) by A14; :: thesis: verum

end;

end;