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 :: thesis: ( ( Low (p,T,i) = 0_ (n,L) & contradiction ) or ( Low (p,T,i) <> 0_ (n,L) & HT ((Low (p,T,i)),T) < HT (p,T),T ) )

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:27, 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 :: thesis: not HT (p,T) in Support (Low (p,T,i))

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

A9: now :: thesis: for u being object st u in Support p holds
u in Support (Low (p,T,i))

let u be object ; :: 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 object 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