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