let n be Ordinal; 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 Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,T
let T be 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 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 ; 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 Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,T
let p be 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 Support (Low (p,T,i)) & b9 in Support (Up (p,T,i)) holds
b < b9,T
let i be Element of NAT ; ( i <= card (Support p) 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 (Support p)
; 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; ( 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)) )
; b < b9,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 < b9,T
by A1, A2, Th20; verum