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
then (numerator p) / (denominator p) = 1 by XCMPLX_1:60;
hence p = 1 by Th12; :: thesis: verum

end;

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