theorem :: XREAL_1:111

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