theorem Th22: :: GROEB_3:22

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