let p be Rational; :: thesis: ( numerator p = - (denominator p) iff p = - 1 )
A1: 0 <> denominator p by Def3;

now

assume numerator p = - (denominator p) ; :: thesis: p = - 1
hence p = (- (denominator p)) / (denominator p) by Th37
.= - ((denominator p) / (denominator p))
.= - 1 by A1, XCMPLX_1:60 ;
:: thesis: verum

end;

hence ( numerator p = - (denominator p) iff p = - 1 ) ; :: thesis: verum