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:
set l = Low p,T,i;
set l1 = Low p,T,(i + 1);
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;
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:47, 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;

let u' be set ; :: thesis:
assume A8: 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 A8, TERMORD:def 6;
hence u' in Support (Low p,T,i) by A1, A7, A4, A6, A5, A8, Th24, TERMORD:8; :: thesis:

end;

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