theorem :: NUMERAL3:85

for a being Rational holds denominator (denominator a) = 1 by NAT_2:def 1;