let x, y be R_eal; :: thesis: ( ( for e being real number st 0 < e holds
x < y + (R_EAL e) ) implies x <= y )
assume A1: for e being real number st 0 < e holds
x < y + (R_EAL 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 + (R_EAL 1) by A1;
hence x <= y by A3, SUPINF_2:def 2; :: 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 + (R_EAL 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, EXTREAL1:41;
reconsider x1 = x as Real by A6, A7, XXREAL_0:14;
reconsider y1 = y as Real by A4, XXREAL_0:14;
A10: x - y = x1 - y1 by SUPINF_2:5;
then x < y + (R_EAL (x1 - y1)) by A1, A9;
then x < (y + x) - y by A10, EXTREAL1:11;
then x < x + (y - y) by A4, EXTREAL1:11;
then x < x + 0. by EXTREAL1:9;
hence contradiction by SUPINF_2:18; :: thesis: verum

end;

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

end;

end;

end;

end;