theorem Th19: :: GROEB_3:19

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
( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} )