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