let a, b, c, d be Real; :: thesis: ( b < 0 & d < 0 & c / d < a * b implies c / b < a * d )
assume that
A1: b < 0 and
A2: d < 0 ; :: thesis: ( not c / d < a * b or c / b < a * d )
assume a * b > c / d ; :: thesis: c / b < a * d
then (a * b) * d < c by A2, Th80;
then (a * d) * b < c ;
hence c / b < a * d by A1, Th82; :: thesis: verum