let a, b, c, d be positive Real; :: thesis: ( a / b < 1 & c / d < 1 implies (a / b) * (c / d) < 1 )
assume a / b < 1 ; :: thesis: ( not c / d < 1 or (a / b) * (c / d) < 1 )
then A1: a < b by XREAL_1:181;
assume c / d < 1 ; :: thesis: (a / b) * (c / d) < 1
then c < d by XREAL_1:181;
then A2: a * c < b * d by A1, XREAL_1:96;
(a / b) * (c / d) = (a * c) / (b * d) by XCMPLX_1:76;
hence (a / b) * (c / d) < 1 by A2, XREAL_1:189; :: thesis: verum