:: deftheorem defines HT GROEB_1:def 1 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) holds HT (P,T) = { (HT (p,T)) where p is Polynomial of n,L : ( p in P & p <> 0_ (n,L) ) } ;