theorem :: TERMORD:36

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds Support (Red (p,T)) = (Support p) \ {(HT (p,T))} by Lm17;