theorem Th23: :: GROEB_3:23

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 non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card (Support p) holds
HT (p,T) in Upper_Support (p,T,i)