consider m2, n2 being Integer such that
n2 <> 0 and
A1: q = m2 / n2 by Th2;
consider m1, n1 being Integer such that
n1 <> 0 and
A2: p = m1 / n1 by Th2;
p * q = (m1 * m2) / (n1 * n2) by A2, A1, XCMPLX_1:76;
hence p * q is rational by Th3; :: thesis: verum