theorem :: XREAL_1:117

for a, b, c, d being Real st 0 < b & d < 0 & c / d < a * b holds
a * d < c / b