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