let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for p being Polynomial of n,L
for i being Element of NAT st i < card () holds
(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

let T be connected admissible 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 () holds
(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),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 () holds
(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i < card () holds
(Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}

let i be Element of NAT ; :: thesis: ( i < card () implies (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))} )
set l = Low (p,T,i);
set l1 = Low (p,T,(i + 1));
assume A1: i < card () ; :: thesis: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))}
then A2: Support (Low (p,T,i)) = Lower_Support (p,T,i) by Lm3;
then A3: card (Support (Low (p,T,i))) = (card ()) - i by ;
now :: thesis: not Lower_Support (p,T,i) = {}
assume Lower_Support (p,T,i) = {} ; :: thesis: contradiction
then (card ()) - i = 0 by ;
hence contradiction by A1; :: thesis: verum
end;
then A4: HT ((Low (p,T,i)),T) in Support (Low (p,T,i)) by ;
A5: Support (Low (p,T,i)) c= Support p by ;
A6: i + 1 <= card () by ;
then Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by Lm3;
then A7: card (Support (Low (p,T,(i + 1)))) = (card ()) - (i + 1) by ;
then card ((Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1))))) = ((card ()) - i) - ((card ()) - (i + 1)) by
.= 1 ;
then consider x being object such that
A8: (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {x} by CARD_2:42;
A9: Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by ;
now :: thesis: not x <> HT ((Low (p,T,i)),T)
assume A10: x <> HT ((Low (p,T,i)),T) ; :: thesis: contradiction
A11: now :: thesis: HT ((Low (p,T,i)),T) in Support (Low (p,T,(i + 1)))
assume not HT ((Low (p,T,i)),T) in Support (Low (p,T,(i + 1))) ; :: thesis: contradiction
then HT ((Low (p,T,i)),T) in (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) by ;
hence contradiction by A8, A10, TARSKI:def 1; :: thesis: verum
end;
A12: now :: thesis: for u being object st u in Support (Low (p,T,i)) holds
u in Support (Low (p,T,(i + 1)))
let u be object ; :: thesis: ( u in Support (Low (p,T,i)) implies u in Support (Low (p,T,(i + 1))) )
assume A13: u in Support (Low (p,T,i)) ; :: thesis: u in Support (Low (p,T,(i + 1)))
then reconsider u9 = u as Element of Bags n ;
u9 <= HT ((Low (p,T,i)),T),T by ;
hence u in Support (Low (p,T,(i + 1))) by A6, A5, A9, A11, A13, Th24; :: thesis: verum
end;
Support (Low (p,T,(i + 1))) c= Support (Low (p,T,i)) by ;
then for u being object st u in Support (Low (p,T,(i + 1))) holds
u in Support (Low (p,T,i)) ;
then (card ()) + (- i) <= (card ()) + (- (i + 1)) by ;
then - i <= - (i + 1) by XREAL_1:6;
then i + 1 <= i by XREAL_1:24;
then (i + 1) - i <= i - i by XREAL_1:9;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum
end;
hence (Support (Low (p,T,i))) \ (Support (Low (p,T,(i + 1)))) = {(HT ((Low (p,T,i)),T))} by A8; :: thesis: verum