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, 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) ) )

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, 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) ) )

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, 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) ) )

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, 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) ) )

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, 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) ) ) )

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, 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) ) )

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, 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) ) )

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: 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)

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

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, 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) ) )

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, 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) ) )

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, 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) ) )

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, 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) ) )

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, 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) ) ) )

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, 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) ) )

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, 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) ) )

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: 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)

now :: thesis: 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)

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)

let b, b9 be bag of n; :: thesis: ( b in Lower_Support (p,T,i) & b9 in Support p & b9 <= b,T implies b9 in Lower_Support (p,T,i) )

assume that

A2: b in Lower_Support (p,T,i) and

A3: b9 in Support p and

A4: b9 <= b,T ; :: thesis: b9 in Lower_Support (p,T,i)

A5: b9 in (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) by A1, A3, Th19;

end;assume that

A2: b in Lower_Support (p,T,i) and

A3: b9 in Support p and

A4: b9 <= b,T ; :: thesis: b9 in Lower_Support (p,T,i)

A5: b9 in (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) by A1, A3, Th19;

now :: thesis: b9 in Lower_Support (p,T,i)

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

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: verum

end;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: verum

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