theorem :: RAT_1:21

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