theorem :: POLYRED:30

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds 0_ (n,L) <= p,T by Lm12;