theorem Th7: :: REAL_3:7

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