let p be Rational; :: thesis: ( - (numerator p) = denominator p iff p = - 1 )
( - (numerator p) = denominator p iff numerator p = - (denominator p) ) ;
hence ( - (numerator p) = denominator p iff p = - 1 ) by Th21; :: thesis: verum