let p be Polynomial of R; :: thesis: ( p is zero implies not p is linear )
assume p is zero ; :: thesis: not p is linear
then p = 0_. R by UPROOTS:def 5;
hence not p is linear by HURWITZ:20; :: thesis: verum