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, b' being bag of st b in Support (Low p,T,i) & b' in Support (Up p,T,i) holds
b < 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, b' being bag of st b in Support (Low p,T,i) & b' in Support (Up p,T,i) holds
b < 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, b' being bag of st b in Support (Low p,T,i) & b' in Support (Up p,T,i) holds
b < b',T
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
for b, b' being bag of st b in Support (Low p,T,i) & b' in Support (Up p,T,i) holds
b < b',T
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies for b, b' being bag of st b in Support (Low p,T,i) & b' in Support (Up p,T,i) holds
b < b',T )
assume A1: i <= card (Support p) ; :: thesis: for b, b' being bag of st b in Support (Low p,T,i) & b' in Support (Up p,T,i) holds
b < b',T
let b, b' be bag of ; :: thesis: ( b in Support (Low p,T,i) & b' in Support (Up p,T,i) implies b < b',T )
assume A2: ( b in Support (Low p,T,i) & b' in Support (Up p,T,i) ) ; :: thesis: b < b',T
( Support (Up p,T,i) = Upper_Support p,T,i & Support (Low p,T,i) = Lower_Support p,T,i ) by A1, Lm3;
hence b < b',T by A1, A2, Th20; :: thesis: verum