let p be Rational; :: thesis: ( numerator p = 0 iff p = 0 )
denominator p <> 0 by Def3;
hence ( numerator p = 0 iff p = 0 ) by XCMPLX_1:6; :: thesis: verum