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

( 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