theorem Th20: :: RAT_1:23

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