for p being Rational st p <> 0 holds
denominator p = (numerator p) / p