theorem :: TERMORD:21

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)) = {} or Support (HM (p,T)) = {(HT (p,T))} ) by Lm12;