theorem Th35: :: GROEB_3:35

for n being Ordinal
for T being connected TermOrder of n
for L being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds
( Up (p,T,(card (Support p))) = p & Low (p,T,(card (Support p))) = 0_ (n,L) )