theorem Th5: :: RAT_1:8

for p being Rational ex m being Integer ex k being Nat st
( k <> 0 & p = m / k )