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