let a, b, c, d be Real; :: thesis: ( b < 0 & 0 < d & 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, Th77;
then (a * d) * b > c ;
hence a * d < c / b by A1, Th84; :: thesis: verum