consider
m
,
n
being
Integer
such that
n
<>
0
and
A1
:
p
=
m
/
n
by
Th2
;

p
=
(

m
)
/
n
by
A1
;
hence

p
is
rational
;
:: thesis:
verum