let x, y be ext-real number ; :: thesis: ( ( for e being real number st 0 < e holds
x < y + e ) implies x <= y )
assume A1: for e being real number st 0 < e holds
x < y + e ; :: thesis: x <= y

per cases ( y = +infty or y = -infty or ( y <> +infty & y <> -infty ) ) ;

suppose A2: ( y = +infty or y = -infty ) ; :: thesis: x <= y

per cases ( y = +infty or y = -infty ) by A2;

suppose y = +infty ; :: thesis: x <= y

hence x <= y by XXREAL_0:4; :: thesis: verum

end;

suppose A3: y = -infty ; :: thesis: x <= y

x < y + 1 by A1;
hence x <= y by A3, Def3; :: thesis: verum

end;

end;

end;

suppose A4: ( y <> +infty & y <> -infty ) ; :: thesis: x <= y

per cases ( x = +infty or x <> +infty ) ;

suppose A5: x = +infty ; :: thesis: x <= y

x < y + 1 by A1;
hence x <= y by A5, XXREAL_0:4; :: thesis: verum

end;

suppose A6: x <> +infty ; :: thesis: x <= y

now

assume A7: x <> -infty ; :: thesis: x <= y
assume A8: not x <= y ; :: thesis: contradiction
( y <= +infty & -infty <= x ) by XXREAL_0:4, XXREAL_0:5;
then ( y < +infty & -infty < x ) by A4, A7, XXREAL_0:1;
then A9: 0 < x - y by A8, Th64;
x in REAL by A6, A7, XXREAL_0:14;
then reconsider x1 = x as real number ;
y in REAL by A4, XXREAL_0:14;
then reconsider y1 = y as real number ;
x < y + (x1 - y1) by A1, A9;
then x < (y + x) - y by Th60;
then x < x + (y - y) by A4, Th60;
then x < x + 0 by Tx4;
hence contradiction by Tx3; :: thesis: verum

end;

hence x <= y by XXREAL_0:5; :: thesis: verum

end;

end;

end;

end;