consider m2, n2 being Integer such that
A3: n2 > 0 and
A4: q = m2 / n2 by Th2;
consider m1, n1 being Integer such that
A5: n1 > 0 and
A6: p = m1 / n1 by Th2;
p + q = ((m1 * n2) + (m2 * n1)) / (n1 * n2) by A5, A6, A3, A4, XCMPLX_1:116;
hence p + q is rational by Th3; :: thesis: verum