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