p <> 0_. R ;
hence deg p is Element of NAT by Th2; :: thesis: verum