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:9;
( a <= max a,b & c <= max c,d ) by XXREAL_0:25;
then a + c <= (max a,b) + (max c,d) by XREAL_1:9;
hence max (a + c),(b + d) <= (max a,b) + (max c,d) by A1, XXREAL_0:28; :: thesis: verum