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