theorem Th11: :: RAT_1:14

for p being Rational holds
( numerator p = 0 iff p = 0 ) by XCMPLX_1:6;