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