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