theorem :: COMPLEX3:55
for a, b, c, d being positive Real st a + b <= c + d & a * b > c * d holds
( max (a,b) < max (c,d) & min (a,b) > min (c,d) )