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

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