let a, b, c, d be Real; 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; verum