for p being Rational holds 1 <= denominator p