theorem :: RAT_1:22

for p being Rational holds
( 1 > (denominator p) " iff not p is integer )