for p being Rational st ( numerator p = p or denominator p = 1 ) & 0 <= p holds
p is Element of NAT