theorem Th27: :: RAT_1:30

for k being Nat
for m being Integer
for p being Rational st p = m / k & k <> 0 & ( for w being Nat holds
( not 1 < w or for m1 being Integer
for k1 being Nat holds
( not m = m1 * w or not k = k1 * w ) ) ) holds
( k = denominator p & m = numerator p )