let r, t be ext-real number ; :: thesis: ( r < t implies ex s being ext-real number st
( r < s & s < t ) )
assume A1: r < t ; :: thesis: ex s being ext-real number 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 ext-real number 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 ext-real number st
( r < s & s < t )

reconsider t = t as real number by A7, XREAL_0:def 1;
consider s being real number such that
A8: s < t by Th4;
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 ext-real number st
( r < s & s < t )

reconsider r9 = r as real number by A9, XREAL_0:def 1;
consider s being real number such that
A11: r9 < s by Th3;
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 ext-real number st
( r < s & s < t )

reconsider r = r, t = t as real number by A12, A13, XREAL_0:def 1;
consider s being real number such that
A14: r < s and
A15: s < t by A1, Th7;
take s ; :: thesis: ( r < s & s < t )
thus ( r < s & s < t ) by A14, A15; :: thesis: verum

end;

end;