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

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