:: deftheorem Def2 defines Upper_Support GROEB_3:def 2 :
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 Nat st i <= card (Support p) holds
for b₆ being finite Subset of (Bags n) holds
( b₆ = Upper_Support (p,T,i) iff ( b₆ c= Support p & card b₆ = i & ( for b, b9 being bag of n st b in b₆ & b9 in Support p & b <= b9,T holds
b9 in b₆ ) ) );