theorem Th40: :: RAT_1:43

for p being Rational holds
( denominator (- p) = denominator p & numerator (- p) = - (numerator p) )