for x, y being Element of REAL
for xe, ye being ExtReal st x <= xe & y <= ye holds
x + y <= xe + ye