theorem Th16: :: POLYRED:16

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L
for b, b9 being bag of n st b9 in Support (b *' p) holds
b9 <= b + (HT (p,T)),T