let b, d, a, c be real number ; :: thesis: ( 0 < b & 0 < d & a * d <= c * b implies a / b <= c / d )
assume that
A1: b > 0 and
A2: d > 0 and
A3: a * d <= c * b ; :: thesis: a / b <= c / d
(a * d) / b <= c by A1, A3, Th81;
then (a / b) * d <= c by XCMPLX_1:75;
hence a / b <= c / d by A2, Th79; :: thesis: verum