theorem :: XXREAL_3:47

for x, y, z being ExtReal st 0 <= x & 0 <= z & z + x < y holds
z < y - x