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

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 )
;

end;

suppose A4:
y <> 0
; :: thesis: x <= z

thus
x <= z
:: thesis: verum

end;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;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