for p being Rational holds
( numerator p = p iff denominator p = 1 ) by Th14;