theorem Th2: :: TOPREAL7:2
for a, b, c, d, e, f being Real st a <= b + c & d <= e + f holds
max (a,d) <= (max (b,e)) + (max (c,f))