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