let n be Ordinal; :: thesis:
let T be connected 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:
set l = Lower_Support (p,T,i);
thus Lower_Support (p,T,i) c= Support p by XBOOLE_1:36; :: thesis:
Upper_Support (p,T,i) c= Support p by A1, Def2;
hence card (Lower_Support (p,T,i)) = (card (Support p)) - (card (Upper_Support (p,T,i))) by CARD_2:44
.= (card (Support p)) - i by A1, Def2 ;
:: thesis:

let b, b9 be bag of n; :: thesis:
assume that
A2: b in Lower_Support (p,T,i) and
A3: b9 in Support p and
A4: b9 <= b,T ; :: thesis:
A5: b9 in (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) by A1, A3, Th19;

assume not b9 in Lower_Support (p,T,i) ; :: thesis:
then b9 in Upper_Support (p,T,i) by A5, XBOOLE_0:def 3;
then b < b9,T by A1, A2, Th20;
hence contradiction by A4, TERMORD:5; :: thesis:

end;

hence b9 in Lower_Support (p,T,i) ; :: thesis:

end;

hence for b, b9 being bag of n st b in Lower_Support (p,T,i) & b9 in Support p & b9 <= b,T holds
b9 in Lower_Support (p,T,i) ; :: thesis: