theorem :: XREAL_1:112
for a, b, c, d being Real st b < 0 & d < 0 & c / d < a * b holds
c / b < a * d