let a, b, c, d be Real; :: thesis: max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d))
( b <= max (a,b) & d <= max (c,d) ) by XXREAL_0:25;
then A1: b + d <= (max (a,b)) + (max (c,d)) by XREAL_1:7;
( a <= max (a,b) & c <= max (c,d) ) by XXREAL_0:25;
then a + c <= (max (a,b)) + (max (c,d)) by XREAL_1:7;
hence max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d)) by A1, XXREAL_0:28; :: thesis: verum