theorem Th45: :: XXREAL_3:45

for x, y, z being ExtReal st x is real holds
( y + x <= z iff y <= z - x )