theorem :: COMPLEX3:59
for a, b, c, d being positive Real st ( ( a * b > c * d & a / b >= c / d ) or ( a * b >= c * d & a / b > c / d ) ) holds
a > c