let x, z be ExtReal; :: thesis:
assume A1: x < z ; :: thesis:

per cases by XXREAL_0:14;

suppose ( x in REAL & z in REAL ) ; :: thesis:

hence ex y being Real st
( x < y & y < z ) by A1, XREAL_1:5; :: thesis:

end;

suppose ( x = +infty or z = -infty ) ; :: thesis:

hence ex y being Real st
( x < y & y < z ) by A1, XXREAL_0:4, XXREAL_0:6; :: thesis:

end;

suppose A2: z = +infty ; :: thesis:

per cases by A1, A2, XXREAL_0:14;

suppose x = -infty ; :: thesis:

hence ex y being Real st
( x < y & y < z ) by A2; :: thesis:

end;

suppose x in REAL ; :: thesis:

then reconsider x1 = x as Real ;
take x1 + 1 ; :: thesis:
A3: x1 + 1 in REAL by XREAL_0:def 1;
x1 + 0 < x1 + 1 by XREAL_1:8;
hence ( x < x1 + 1 & x1 + 1 < z ) by A2, A3, XXREAL_0:9; :: thesis:

end;

end;

end;

suppose A4: x = -infty ; :: thesis:

per cases by A1, A4, XXREAL_0:14;

suppose z = +infty ; :: thesis:

hence ex y being Real st
( x < y & y < z ) by A4; :: thesis:

end;

suppose z in REAL ; :: thesis:

then reconsider z1 = z as Real ;
take z1 - 1 ; :: thesis:
A5: z1 - 1 in REAL by XREAL_0:def 1;
z1 - 1 < z1 - 0 by XREAL_1:10;
hence ( x < z1 - 1 & z1 - 1 < z ) by A4, A5, XXREAL_0:12; :: thesis:

end;

end;

end;

end;