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 & t <> -infty ) by XXREAL_0:3, 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, XXREAL_0:14;

suppose that A3: r = -infty and
A4: 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 A3, A4; :: thesis: verum

end;

suppose that A5: r = -infty and
A6: t in REAL ; :: thesis: ex s being ext-real number st
( r < s & s < t )

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

end;

suppose that A8: r in REAL and
A9: t = +infty ; :: thesis: ex s being ext-real number st
( r < s & s < t )

reconsider r' = r as real number by A8, XREAL_0:def 1;
consider s being real number such that
A10: r' < s by Th3;
take s ; :: thesis: ( r < s & s < t )
thus r < s by A10; :: thesis: s < t
s in REAL by XREAL_0:def 1;
hence s < t by A9, XXREAL_0:9; :: thesis: verum

end;

suppose that A11: r in REAL and
A12: t in REAL ; :: thesis: ex s being ext-real number st
( r < s & s < t )

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

end;

end;