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