LC
(
p
*'
q
)
=
(
LC
p
)
*
(
LC
q
)
by
NIVEN:46
.=
(
LC
p
)
*
(
1.
R
)
by
RATFUNC1:def 7
.=
(
1.
R
)
*
(
1.
R
)
by
RATFUNC1:def 7
;
hence
p
*'
q
is
monic
;
:: thesis:
verum