consider m2, n2 being Integer such that
A7: n2 <> 0 and
A8: q = m2 / n2 by Th3;
consider m1, n1 being Integer such that
A9: n1 <> 0 and
A10: p = m1 / n1 by Th3;
p - q = ((m1 * n2) - (m2 * n1)) / (n1 * n2) by A9, A10, A7, A8, XCMPLX_1:131;
hence p - q is rational by Th6; :: thesis: verum