theorem LMINEQ: :: NORMSP_3:22

for x, y, z being Real st 0 <= y & ( for e being Real st 0 < e holds
x <= z + (y * e) ) holds
x <= z