consider m1, n1 being Integer such that

n1 <> 0 and

A11: p = m1 / n1 by Th2;

consider m2, n2 being Integer such that

n2 <> 0 and

A12: q = m2 / n2 by Th2;

p / q = p * (1 / (m2 / n2)) by A12

.= p * ((1 * n2) / m2) by XCMPLX_1:77

.= (m1 * n2) / (n1 * m2) by A11, XCMPLX_1:76 ;

hence p / q is rational by Th3; :: thesis: verum

n1 <> 0 and

A11: p = m1 / n1 by Th2;

consider m2, n2 being Integer such that

n2 <> 0 and

A12: q = m2 / n2 by Th2;

p / q = p * (1 / (m2 / n2)) by A12

.= p * ((1 * n2) / m2) by XCMPLX_1:77

.= (m1 * n2) / (n1 * m2) by A11, XCMPLX_1:76 ;

hence p / q is rational by Th3; :: thesis: verum