theorem Th31: :: IRRAT_1:31

for x being Real st x is rational holds
ex n being Nat st
( n >= 2 & (n !) * x is integer )