theorem :: COMPLEX3:56

for a, b, c, d being positive Real holds
( max (a,b) = max (c,d) & min (a,b) = min (c,d) iff ( a * b = c * d & a + b = c + d ) )