theorem Th24: :: RAT_1:27

for k being Nat
for m being Integer
for p being Rational st k <> 0 & p = m / k holds
ex w being Nat st
( m = (numerator p) * w & k = (denominator p) * w )