theorem Th6: :: HILB10_5:7

for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p holds
degree p >= degree b