let a, b, c, d be Real; :: thesis: ( b < 0 & d < 0 & 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, Th80;
then (a / b) * d >= c by XCMPLX_1:74;
hence a / b <= c / d by A2, Th80; :: thesis: verum