let n be Ordinal; :: thesis: for T being connected 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
( Lower_Support p,T,i c= Support p & card (Lower_Support p,T,i) = (card (Support p)) - i & ( for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support p,T,i ) )
let T be connected 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
( Lower_Support p,T,i c= Support p & card (Lower_Support p,T,i) = (card (Support p)) - i & ( for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support 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
( Lower_Support p,T,i c= Support p & card (Lower_Support p,T,i) = (card (Support p)) - i & ( for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support p,T,i ) )
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
( Lower_Support p,T,i c= Support p & card (Lower_Support p,T,i) = (card (Support p)) - i & ( for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support p,T,i ) )
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies ( Lower_Support p,T,i c= Support p & card (Lower_Support p,T,i) = (card (Support p)) - i & ( for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support p,T,i ) ) )
assume A1: i <= card (Support p) ; :: thesis: ( Lower_Support p,T,i c= Support p & card (Lower_Support p,T,i) = (card (Support p)) - i & ( for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support p,T,i ) )
set l = Lower_Support p,T,i;
thus Lower_Support p,T,i c= Support p by XBOOLE_1:36; :: thesis: ( card (Lower_Support p,T,i) = (card (Support p)) - i & ( for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support p,T,i ) )
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:63
.= (card (Support p)) - i by A1, Def2 ;
:: thesis: for b, b' being bag of n st b in Lower_Support p,T,i & b' in Support p & b' <= b,T holds
b' in Lower_Support p,T,i

now

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

now

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

end;

hence b' in Lower_Support p,T,i ; :: thesis: verum

end;

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