let p, q be Rational; :: thesis: p / q is Rational
consider m1, n1 being Integer such that
n1 <> 0 and
A1: p = m1 / n1 by Th3;
consider m2, n2 being Integer such that
n2 <> 0 and
A2: q = m2 / n2 by Th3;
p / q = p * (1 / (m2 / n2)) by A2
.= p * ((1 * n2) / m2) by XCMPLX_1:77
.= (m1 * n2) / (n1 * m2) by A1, XCMPLX_1:76 ;
hence p / q is Rational by Th6; :: thesis: verum