theorem Th26: :: RAT_1:29

for p being Rational
for w being Nat holds
( not 1 < w or for m being Integer
for k being Nat holds
( not numerator p = m * w or not denominator p = k * w ) )