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

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

thus
( p = 1 implies numerator p = denominator p )
; :: thesis: verumassume
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;then (numerator p) / (denominator p) = 1 by XCMPLX_1:60;

hence p = 1 by Th12; :: thesis: verum