theorem Th42: :: GROEB_3:42

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i < card (Support p) holds
(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}