let p be Rational; :: thesis: ( numerator p = - (denominator p) iff p = - 1 )

hereby :: thesis: ( p = - 1 implies numerator p = - (denominator p) )

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

end;

thus ( p = - 1 implies numerator p = - (denominator p) ) ; :: thesis: verum