let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card (Support p) holds
Support (Low (p,T,i)) c= Support (Red (p,T))
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card (Support p) holds
Support (Low (p,T,i)) c= Support (Red (p,T))
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card (Support p) holds
Support (Low (p,T,i)) c= Support (Red (p,T))
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st 1 <= i & i <= card (Support p) holds
Support (Low (p,T,i)) c= Support (Red (p,T))
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= card (Support p) implies Support (Low (p,T,i)) c= Support (Red (p,T)) )
assume that
A1: 1 <= i and
A2: i <= card (Support p) ; :: thesis: Support (Low (p,T,i)) c= Support (Red (p,T))
Support p <> {} by A1, A2;
then p <> 0_ (n,L) by POLYNOM7:1;
then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;
set sl = Lower_Support (p,T,i);

A3: now :: thesis: not HT (p,T) in Lower_Support (p,T,i)

assume A4: HT (p,T) in Lower_Support (p,T,i) ; :: thesis: contradiction
HT (p,T) in Upper_Support (p,T,i) by A1, A2, 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 A2, Th19; :: thesis: verum

end;

now :: thesis: not {(HT (p,T))} /\ (Lower_Support (p,T,i)) <> {}

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

end;

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