let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty 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: i < card (Support p) ; :: thesis:
then A2: i + 1 <= card (Support p) by NAT_1:13;
then A3: (card (Support p)) - i >= 1 by XREAL_1:21;
set l = Low p,T,i;
set l1 = Low p,T,(i + 1);
A4: Support (Low p,T,(i + 1)) c= Support p by A2, Th26;
A5: Support (Low p,T,i) = Lower_Support p,T,i by A1, Lm3;
then A6: card (Support (Low p,T,i)) = (card (Support p)) - i by A1, Th24;
A7: HT (Low p,T,(i + 1)),T <= HT (Low p,T,i),T,T by A1, Th38;
A8: HT (Low p,T,i),T in Lower_Support p,T,i by A3, A5, A6, CARD_1:47, TERMORD:def 6;

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

end;

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