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