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