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
( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (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
( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (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
( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} )
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} )
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies ( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} ) )
set M = (Upper_Support (p,T,i)) /\ ((Support p) \ (Upper_Support (p,T,i)));
assume i <= card (Support p) ; :: thesis: ( (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = Support p & (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} )
then A1: Upper_Support (p,T,i) c= Support p by Def2;
thus (Upper_Support (p,T,i)) \/ (Lower_Support (p,T,i)) = (Upper_Support (p,T,i)) \/ (Support p) by XBOOLE_1:39
.= Support p by A1, XBOOLE_1:12 ; :: thesis: (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {}
now :: thesis: not (Upper_Support (p,T,i)) /\ ((Support p) \ (Upper_Support (p,T,i))) <> {}
set x = the Element of (Upper_Support (p,T,i)) /\ ((Support p) \ (Upper_Support (p,T,i)));
assume (Upper_Support (p,T,i)) /\ ((Support p) \ (Upper_Support (p,T,i))) <> {} ; :: thesis: contradiction
then ( the Element of (Upper_Support (p,T,i)) /\ ((Support p) \ (Upper_Support (p,T,i))) in Upper_Support (p,T,i) & the Element of (Upper_Support (p,T,i)) /\ ((Support p) \ (Upper_Support (p,T,i))) in (Support p) \ (Upper_Support (p,T,i)) ) by XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
hence (Upper_Support (p,T,i)) /\ (Lower_Support (p,T,i)) = {} ; :: thesis: verum