theorem :: TERMORD:17

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC (p,T) = 0. L iff p = 0_ (n,L) ) by Lm7;