for p being Rational holds 1 >= (denominator p) "