theorem :: XXREAL_3:35

for x, y, z being ExtReal st x <= y holds
x + z <= y + z by Lm12;