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
for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds
b9 < b,T
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
for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds
b9 < b,T
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
for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds
b9 < b,T
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds
b9 < b,T
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds
b9 < b,T )
assume A1: i <= card (Support p) ; :: thesis: for b, b9 being bag of n st b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) holds
b9 < b,T
let b, b9 be bag of n; :: thesis: ( b in Upper_Support (p,T,i) & b9 in Lower_Support (p,T,i) implies b9 < b,T )
assume that
A2: b in Upper_Support (p,T,i) and
A3: b9 in Lower_Support (p,T,i) ; :: thesis: b9 < b,T
A4: Lower_Support (p,T,i) c= Support p by XBOOLE_1:36;

now :: thesis: not b <= b9,T

assume b <= b9,T ; :: thesis: contradiction
then b9 in Upper_Support (p,T,i) by A1, A2, A3, A4, Def2;
then b9 in (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) by A3, XBOOLE_0:def 4;
hence contradiction by A1, Th19; :: thesis: verum

end;

hence b9 < b,T by TERMORD:5; :: thesis: verum