let n be Ordinal; :: thesis: for T being connected TermOrder of n
for p being Polynomial of n,L
for i being Element of NAT st 0 < i & i < card () 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 () 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 () 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 () holds
HT ((Low (p,T,i)),T) < HT (p,T),T

let i be Element of NAT ; :: thesis: ( 0 < i & i < card () implies HT ((Low (p,T,i)),T) < HT (p,T),T )
assume that
A1: 0 < i and
A2: i < card () ; :: 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 ;
Support (Low (p,T,i)) = Lower_Support (p,T,i) by ;
then 0 + i = ((card ()) - 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 ;
A6: Support (Low (p,T,i)) = Lower_Support (p,T,i) by ;
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 ;
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 () = card (Support (Low (p,T,i))) by
.= (card ()) - i by A2, A6, Th24 ;
hence contradiction by A1; :: thesis: verum
end;
Support (Low (p,T,i)) <> {} by ;
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 ;
hence HT ((Low (p,T,i)),T) < HT (p,T),T by ; :: thesis: verum
end;
end;
end;
hence HT ((Low (p,T,i)),T) < HT (p,T),T ; :: thesis: verum