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