theorem :: SQUARE_1:1

for x, y being Real holds (min (x,y)) + (max (x,y)) = x + y