theorem Th6: :: RAT_1:9

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