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