for n being Ordinal
for T being connected 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
for b being bag of n st b in Support p holds
( ( b in Support (Up (p,T,i)) or b in Support (Low (p,T,i)) ) & not b in (Support (Up (p,T,i))) /\ (Support (Low (p,T,i))) )