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