theorem Th1: :: TOPREAL7:1

for a, b, c, d being Real holds max ((a + c),(b + d)) <= (max (a,b)) + (max (c,d))