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
end;
suppose A4: ( y <> +infty & y <> -infty ) ; :: thesis: x <= y
per cases ( x = +infty or x <> +infty ) ;
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;