theorem :: XXREAL_3:40

for x, y being ExtReal st x <= y holds
y - x >= 0