for p being Rational st p >= 0 holds
ex m, n being Nat st
( n <> 0 & p = m / n )