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