theorem Th2: :: FIELD_1:1

for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )