:: deftheorem Def6 defines HT TERMORD:def 6 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L
for b₅ being Element of Bags n holds
( b₅ = HT (p,T) iff ( ( Support p = {} & b₅ = EmptyBag n ) or ( b₅ in Support p & ( for b being bag of n st b in Support p holds
b <= b₅,T ) ) ) );