let x, y, z be Real; :: thesis: ( 0 <= y & ( for e being Real st 0 < e holds
x <= z + (y * e) ) implies x <= z )
assume that
A1: 0 <= y and
A2: for e being Real st 0 < e holds
x <= z + (y * e) ; :: thesis: x <= z
per cases ( y = 0 or y <> 0 ) ;
suppose A3: y = 0 ; :: thesis: x <= z
x <= z + (y * 1) by A2;
hence x <= z by A3; :: thesis: verum
end;
suppose A4: y <> 0 ; :: thesis: x <= z
thus x <= z :: thesis: verum
proof
assume not x <= z ; :: thesis: contradiction
then A6: 0 < x - z by XREAL_1:50;
then x <= z + (y * (((x - z) / 2) / y)) by A1, A2, A4;
then A7: x <= z + ((y * ((x - z) / 2)) / y) by XCMPLX_1:74;
(x - z) / 2 < x - z by A6, XREAL_1:216;
then z + ((x - z) / 2) < z + (x - z) by XREAL_1:8;
hence contradiction by A4, A7, XCMPLX_1:89; :: thesis: verum
end;
end;
end;