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