for p, q being Rational holds
( p < q iff (numerator p) * (denominator q) < (numerator q) * (denominator p) )