let n be Ordinal; :: thesis: for T being connected admissible 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
(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 (Support p) 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 (Support p) 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 (Support p) 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 (Support p) implies (Support (Low p,T,i)) \ (Support (Low p,T,(i + 1))) = {(HT (Low p,T,i),T)} )
assume A1: i < card (Support p) ; :: thesis: (Support (Low p,T,i)) \ (Support (Low p,T,(i + 1))) = {(HT (Low p,T,i),T)}
then A2: i + 1 <= card (Support p) by NAT_1:13;
set l = Low p,T,i;
set l1 = Low p,T,(i + 1);
A3: Support (Low p,T,i) c= Support p by A1, Th26;
A4: Support (Low p,T,(i + 1)) = Lower_Support p,T,(i + 1) by A2, Lm3;
A5: Support (Low p,T,i) = Lower_Support p,T,i by A1, Lm3;
A6: Support (Low p,T,(i + 1)) = Lower_Support p,T,(i + 1) by A2, Lm3;
A7: card (Support (Low p,T,i)) = (card (Support p)) - i by A1, A5, Th24;
A8: card (Support (Low p,T,(i + 1))) = (card (Support p)) - (i + 1) by A2, A6, Th24;

now

assume Lower_Support p,T,i = {} ; :: thesis: contradiction
then (card (Support p)) - i = 0 by A1, Th24, CARD_1:47;
hence contradiction by A1; :: thesis: verum

end;

then A9: HT (Low p,T,i),T in Support (Low p,T,i) by A5, TERMORD:def 6;
card ((Support (Low p,T,i)) \ (Support (Low p,T,(i + 1)))) = ((card (Support p)) - i) - ((card (Support p)) - (i + 1)) by A1, A7, A8, Th41, CARD_2:63
.= 1 ;
then consider x being set such that
A10: (Support (Low p,T,i)) \ (Support (Low p,T,(i + 1))) = {x} by CARD_2:60;

now

assume A11: x <> HT (Low p,T,i),T ; :: thesis: contradiction

A12: now

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 A9, XBOOLE_0:def 5;
hence contradiction by A10, A11, TARSKI:def 1; :: thesis: verum

end;

A13: now

let u be set ; :: thesis: ( u in Support (Low p,T,i) implies u in Support (Low p,T,(i + 1)) )
assume A14: u in Support (Low p,T,i) ; :: thesis: u in Support (Low p,T,(i + 1))
then reconsider u' = u as Element of Bags n ;
u' <= HT (Low p,T,i),T,T by A14, TERMORD:def 6;
hence u in Support (Low p,T,(i + 1)) by A2, A3, A4, A12, A14, Th24; :: thesis: verum

end;

Support (Low p,T,(i + 1)) c= Support (Low p,T,i) by A1, Th41;
then for u being set st u in Support (Low p,T,(i + 1)) holds
u in Support (Low p,T,i) ;
then (card (Support p)) + (- i) <= (card (Support p)) + (- (i + 1)) by A7, A8, A13, TARSKI:2;
then - i <= - (i + 1) by XREAL_1:8;
then i + 1 <= i by XREAL_1:26;
then (i + 1) - i <= i - i by XREAL_1:11;
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 A10; :: thesis: verum