let a, b, c, d, e, f be Real; :: thesis: ( a <= b + c & d <= e + f implies max (a,d) <= (max (b,e)) + (max (c,f)) )
assume ( a <= b + c & d <= e + f ) ; :: thesis: max (a,d) <= (max (b,e)) + (max (c,f))
then A1: max (a,d) <= max ((b + c),(e + f)) by XXREAL_0:26;
max ((b + c),(e + f)) <= (max (b,e)) + (max (c,f)) by Th1;
hence max (a,d) <= (max (b,e)) + (max (c,f)) by A1, XXREAL_0:2; :: thesis: verum