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

now :: thesis: ( numerator p = denominator p implies p = 1 )

assume numerator p = denominator p ; :: thesis: p = 1
then (numerator p) / (denominator p) = 1 by A1, XCMPLX_1:60;
hence p = 1 by Th12; :: thesis: verum

end;

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