let r, s be real number ; :: thesis: max+ (r + s) <= (max+ r) + (max+ s)
A1: ( 0 <= max r,0 & 0 <= max s,0 ) by XXREAL_0:25;
A2: ( r <= max r,0 & s <= max s,0 ) by XXREAL_0:25;

now

per cases ( 0 <= r + s or r + s < 0 ) ;

case 0 <= r + s ; :: thesis: max+ (r + s) <= (max+ r) + (max+ s)

then max+ (r + s) = r + s by XXREAL_0:def 10;
hence max+ (r + s) <= (max+ r) + (max+ s) by A2, XREAL_1:9; :: thesis: verum

end;

case r + s < 0 ; :: thesis: max+ (r + s) <= (max+ r) + (max+ s)

then max+ (r + s) = 0 + 0 by XXREAL_0:def 10;
hence max+ (r + s) <= (max+ r) + (max+ s) by A1; :: thesis: verum

end;

end;

end;

hence max+ (r + s) <= (max+ r) + (max+ s) ; :: thesis: verum