let x, y be Element of REAL ; :: thesis: for xe, ye being ExtReal st x <= xe & y <= ye holds
x + y <= xe + ye
let xe, ye be ExtReal; :: thesis: ( x <= xe & y <= ye implies x + y <= xe + ye )
assume that
A1: x <= xe and
A2: y <= ye ; :: thesis: x + y <= xe + ye
reconsider x1 = x, y1 = y as ExtReal ;
x1 + y1 <= xe + ye by A1, A2, XXREAL_3:36;
hence x + y <= xe + ye by XXREAL_3:def 2; :: thesis: verum