let q, p be Real; :: thesis: ( q <> 0 implies ex y being Real st p = q * y )
reconsider y = p / q as Real ;
assume A1: q <> 0 ; :: thesis: ex y being Real st p = q * y
take y ; :: thesis: p = q * y
thus p = q * y by A1, XCMPLX_1:87; :: thesis: verum