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