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 Th2;
hence max a,d <= (max b,e) + (max c,f) by A1, XXREAL_0:2; :: thesis: verum