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