let x, y be ExtReal; :: thesis: ( ( for e being Real st 0 < e holds
x < y + e ) implies x <= y )
assume A1: for e being Real 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, Def2; :: 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 :: thesis: ( x <> -infty implies x <= y )

assume A7: x <> -infty ; :: thesis: x <= y
then x in REAL by A6, XXREAL_0:14;
then reconsider x1 = x as Real ;
-infty <= x by XXREAL_0:5;
then A8: -infty < x by A7, XXREAL_0:1;
y in REAL by A4, XXREAL_0:14;
then reconsider y1 = y as Real ;
assume A9: not x <= y ; :: thesis: contradiction
y < +infty by A4, XXREAL_0:4;
then 0 < x - y by A9, A8, Th51;
then x < y + (x1 - y1) by A1;
then x < (y + x) - y by Th30;
then x < x + (y - y) by A4, Th30;
then x < x + 0 by Th7;
hence contradiction by Th4; :: thesis: verum

end;

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

end;

end;

end;

end;