let n be Ordinal; :: thesis: for T being connected admissible 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 Element of NAT st i < card (Support p) holds
Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))
let T be connected admissible TermOrder of n; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i < card (Support p) holds
Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L
for i being Element of NAT st i < card (Support p) holds
Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i < card (Support p) holds
Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))
let i be Element of NAT ; :: thesis: ( i < card (Support p) implies Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i)) )
set l = Low (p,T,i);
set l1 = Low (p,T,(i + 1));
assume A1: i < card (Support p) ; :: thesis: Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i))
then A2: i + 1 <= card (Support p) by NAT_1:13;
then A3: (card (Support p)) - i >= 1 by XREAL_1:19;
A4: Support (Low (p,T,i)) = Lower_Support (p,T,i) by A1, Lm3;
then card (Support (Low (p,T,i))) = (card (Support p)) - i by A1, Th24;
then A5: HT ((Low (p,T,i)),T) in Lower_Support (p,T,i) by A3, A4, CARD_1:27, TERMORD:def 6;
A6: HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T by A1, Th38;
A7: Support (Low (p,T,(i + 1))) c= Support p by A2, Th26;

now

let u9 be set ; :: thesis: ( u9 in Support (Low (p,T,(i + 1))) implies u9 in Support (Low (p,T,i)) )
assume A8: u9 in Support (Low (p,T,(i + 1))) ; :: thesis: u9 in Support (Low (p,T,i))
then reconsider u = u9 as Element of Bags n ;
u <= HT ((Low (p,T,(i + 1))),T),T by A8, TERMORD:def 6;
hence u9 in Support (Low (p,T,i)) by A1, A7, A4, A6, A5, A8, Th24, TERMORD:8; :: thesis: verum

end;

hence Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i)) by TARSKI:def 3; :: thesis: verum