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

consider x being 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 ( x in Upper_Support p,T,i & x 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