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