let n be Ordinal; :: thesis:
let T be connected TermOrder of n; :: thesis:
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis:
let p be Polynomial of n,L; :: thesis:
let i be Element of NAT ; :: thesis:
assume A1: ( 1 <= i & i <= card (Support p) ) ; :: thesis:
then Support p <> {} ;
then p <> 0_ n,L by POLYNOM7:1;
then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 2;
set sl = Lower_Support p,T,i;
Support (Low p,T,i) c= Support p by A1, Th26;
then (Support (Low p,T,i)) \ {(HT p,T)} c= (Support p) \ {(HT p,T)} by XBOOLE_1:33;
then A2: (Support (Low p,T,i)) \ {(HT p,T)} c= Support (Red p,T) by TERMORD:36;

A3: now

assume A4: HT p,T in Lower_Support p,T,i ; :: thesis:
HT p,T in Upper_Support p,T,i by A1, Th23;
then HT p,T in (Upper_Support p,T,i) /\ (Lower_Support p,T,i) by A4, XBOOLE_0:def 4;
hence contradiction by A1, Th19; :: thesis:

end;

now

assume A5: {(HT p,T)} /\ (Lower_Support p,T,i) <> {} ; :: thesis:
consider u being Element of {(HT p,T)} /\ (Lower_Support p,T,i);
( u in {(HT p,T)} & u in Lower_Support p,T,i ) by A5, XBOOLE_0:def 4;
hence contradiction by A3, TARSKI:def 1; :: thesis:

end;

then {(HT p,T)} misses Lower_Support p,T,i by XBOOLE_0:def 7;
then (Lower_Support p,T,i) \ {(HT p,T)} = Lower_Support p,T,i by XBOOLE_1:83
.= Support (Low p,T,i) by A1, Lm3 ;
hence Support (Low p,T,i) c= Support (Red p,T) by A1, A2, Lm3; :: thesis: