let n be Ordinal; :: thesis: for T being connected TermOrder of n
for p being Polynomial of n,L
for i being Element of NAT st i <= card () holds
for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,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 () holds
for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,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 () holds
for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,T

let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i <= card () holds
for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,T

let i be Element of NAT ; :: thesis: ( i <= card () implies for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,T )

assume A1: i <= card () ; :: thesis: for b, b9 being bag of n st b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,T

let b, b9 be bag of n; :: thesis: ( b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) implies b < b9,T )
assume A2: ( b in Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) ) ; :: thesis: b < b9,T
( Support (Up (p,T,i)) = Upper_Support (p,T,i) & Support (Low (p,T,i)) = Lower_Support (p,T,i) ) by ;
hence b < b9,T by A1, A2, Th20; :: thesis: verum