theorem :: RAT_1:28

for m, n being Integer
for p being Rational st p = m / n & n <> 0 holds
ex m1 being Integer st
( m = (numerator p) * m1 & n = (denominator p) * m1 )