let r, s be Real; :: 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 :: thesis: ( ( 0 <= r + s & max+ (r + s) <= (max+ r) + (max+ s) ) or ( r + s < 0 & max+ (r + s) <= (max+ r) + (max+ s) ) )

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:7; :: 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