theorem :: TERMORD:20

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds Support (HM (p,T)) c= Support p