theorem :: XXREAL_3:65

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