:: deftheorem defines Lower_Support GROEB_3:def 3 :
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 holds Lower_Support (p,T,i) = (Support p) \ (Upper_Support (p,T,i));