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 0 < i & i < card (Support p) holds
HT (Low p,T,i),T < HT p,T,T
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 0 < i & i < card (Support p) holds
HT (Low p,T,i),T < HT p,T,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 0 < i & i < card (Support p) holds
HT (Low p,T,i),T < HT p,T,T
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st 0 < i & i < card (Support p) holds
HT (Low p,T,i),T < HT p,T,T
let i be Element of NAT ; :: thesis: ( 0 < i & i < card (Support p) implies HT (Low p,T,i),T < HT p,T,T )
assume A1: ( 0 < i & i < card (Support p) ) ; :: thesis: HT (Low p,T,i),T < HT p,T,T
set l = Low p,T,i;

now

per cases ( Low p,T,i = 0_ n,L or Low p,T,i <> 0_ n,L ) ;

case Low p,T,i = 0_ n,L ; :: thesis: contradiction

then A2: card (Support (Low p,T,i)) = 0 by CARD_1:47, POLYNOM7:1;
Support (Low p,T,i) = Lower_Support p,T,i by A1, Lm3;
then 0 + i = ((card (Support p)) - i) + i by A1, A2, Th24;
hence contradiction by A1; :: thesis: verum

end;

case Low p,T,i <> 0_ n,L ; :: thesis: HT (Low p,T,i),T < HT p,T,T

then A3: Support (Low p,T,i) <> {} by POLYNOM7:1;
A4: Support (Low p,T,i) c= Support p by A1, Th26;
A5: Support (Low p,T,i) = Lower_Support p,T,i by A1, Lm3;

A6: now

assume A7: HT p,T in Support (Low p,T,i) ; :: thesis: contradiction
A8: for u being set st u in Support (Low p,T,i) holds
u in Support p by A4;

now

let u be set ; :: thesis: ( u in Support p implies u in Support (Low p,T,i) )
assume A9: u in Support p ; :: thesis: u in Support (Low p,T,i)
then reconsider x = u as Element of Bags n ;
x <= HT p,T,T by A9, TERMORD:def 6;
hence u in Support (Low p,T,i) by A1, A5, A7, A9, Th24; :: thesis: verum

end;

then card (Support p) = card (Support (Low p,T,i)) by A8, TARSKI:2
.= (card (Support p)) - i by A1, A5, Th24 ;
hence contradiction by A1; :: thesis: verum

end;

A10: HT (Low p,T,i),T in Support (Low p,T,i) by A3, TERMORD:def 6;
then HT (Low p,T,i),T <= HT p,T,T by A4, TERMORD:def 6;
hence HT (Low p,T,i),T < HT p,T,T by A6, A10, TERMORD:def 3; :: thesis: verum

end;

end;

end;

hence HT (Low p,T,i),T < HT p,T,T ; :: thesis: verum