for p being Rational holds 0 < denominator p