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 that
A1: 0 < i and
A2: 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 A3: card (Support (Low p,T,i)) = 0 by CARD_1:47, POLYNOM7:1;
Support (Low p,T,i) = Lower_Support p,T,i by A2, Lm3;
then 0 + i = ((card (Support p)) - i) + i by A2, A3, Th24;
hence contradiction by A2; :: thesis: verum

end;

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

A5: Support (Low p,T,i) c= Support p by A2, Th26;
A6: Support (Low p,T,i) = Lower_Support p,T,i by A2, Lm3;

A7: now

assume A8: HT p,T in Support (Low p,T,i) ; :: thesis: contradiction

A9: now

let u be set ; :: thesis: ( u in Support p implies u in Support (Low p,T,i) )
assume A10: 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 A10, TERMORD:def 6;
hence u in Support (Low p,T,i) by A2, A6, A8, A10, Th24; :: thesis: verum

end;

for u being set st u in Support (Low p,T,i) holds
u in Support p by A5;
then card (Support p) = card (Support (Low p,T,i)) by A9, TARSKI:2
.= (card (Support p)) - i by A2, A6, Th24 ;
hence contradiction by A1; :: thesis: verum

end;

Support (Low p,T,i) <> {} by A4, POLYNOM7:1;
then A11: HT (Low p,T,i),T in Support (Low p,T,i) by TERMORD:def 6;
then HT (Low p,T,i),T <= HT p,T,T by A5, TERMORD:def 6;
hence HT (Low p,T,i),T < HT p,T,T by A7, A11, TERMORD:def 3; :: thesis: verum

end;

end;

end;

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