let p, q be Rational; :: thesis: ( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) )
A1: ( 0 < denominator p & 0 < denominator q ) by Th27;
( p < q iff (numerator p) / (denominator p) < q ) by Th37;
then ( p < q iff (numerator p) / (denominator p) < (numerator q) / (denominator q) ) by Th37;
hence ( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) ) by A1, XREAL_1:104, XREAL_1:108; :: thesis: verum