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