theorem FRA: :: NUMERAL3:97

for a being Rational holds denominator (frac a) = denominator (frac (- a))