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