theorem ISM: :: COMPLEX3:41
for a, b, c, d being positive Real st a + b = c + d & a * b = c * d holds
max (a,b) = max (c,d)