theorem :: XREAL_1:106

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