take
1_.
R
;
:: thesis:
(
1_.
R
is
monic
& not
1_.
R
is
with_roots
)
thus
(
1_.
R
is
monic
& not
1_.
R
is
with_roots
) ;
:: thesis:
verum