for p being Rational holds 0 < (denominator p) " ;