A1: denominator p <> 0 by Def3;
ex m being Integer st p = m / (denominator p) by Def3;
hence (denominator p) * p is Integer by A1, XCMPLX_1:87; :: thesis: verum