theorem :: SQUARE_1:2

for x, y being Real st 0 <= x & 0 <= y holds
max (x,y) <= x + y