let n be Ordinal; :: thesis: for T being connected TermOrder of n
for p being non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card () holds
HT (p,T) in Upper_Support (p,T,i)

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card () holds
HT (p,T) in Upper_Support (p,T,i)

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card () holds
HT (p,T) in Upper_Support (p,T,i)

let p be non-zero Polynomial of n,L; :: thesis: for i being Element of NAT st 1 <= i & i <= card () holds
HT (p,T) in Upper_Support (p,T,i)

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= card () implies HT (p,T) in Upper_Support (p,T,i) )
assume that
A1: 1 <= i and
A2: i <= card () ; :: thesis: HT (p,T) in Upper_Support (p,T,i)
p <> 0_ (n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then A3: HT (p,T) in Support p by TERMORD:def 6;
set u = Upper_Support (p,T,i);
set x = the Element of Upper_Support (p,T,i);
A4: Upper_Support (p,T,i) <> {} by ;
then A5: the Element of Upper_Support (p,T,i) in Upper_Support (p,T,i) ;
then reconsider x9 = the Element of Upper_Support (p,T,i) as Element of Bags n ;
Upper_Support (p,T,i) c= Support p by ;
then x9 <= HT (p,T),T by ;
hence HT (p,T) in Upper_Support (p,T,i) by A2, A4, A3, Def2; :: thesis: verum