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
HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),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
HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),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 i < card (Support p) holds
HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st i < card (Support p) holds
HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T
let i be Element of NAT ; :: thesis: ( i < card (Support p) implies HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T )
set li = Low (p,T,i);
set li1 = Low (p,T,(i + 1));
assume A1: i < card (Support p) ; :: thesis: HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T
then Support (Low (p,T,i)) = Lower_Support (p,T,i) by Lm3;
then A2: card (Support (Low (p,T,i))) = (card (Support p)) - i by A1, Th24;
A3: i + 1 <= card (Support p) by A1, NAT_1:13;
then A4: Support (Low (p,T,(i + 1))) = Lower_Support (p,T,(i + 1)) by Lm3;
then A5: card (Support (Low (p,T,(i + 1)))) = (card (Support p)) - (i + 1) by A3, Th24;
A6: Support (Low (p,T,i)) c= Support p by A1, Th26;

now

per cases ( i = (card (Support p)) - 1 or i <> (card (Support p)) - 1 ) ;

case i = (card (Support p)) - 1 ; :: thesis: HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T

then card (Support (Low (p,T,(i + 1)))) = (card (Support p)) - (card (Support p)) by A4, Th24
.= 0 ;
then Support (Low (p,T,(i + 1))) = {} ;
then HT ((Low (p,T,(i + 1))),T) = EmptyBag n by TERMORD:def 6;
hence HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T by TERMORD:9; :: thesis: verum

end;

case i <> (card (Support p)) - 1 ; :: thesis: HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T

then card (Lower_Support (p,T,(i + 1))) <> 0 by A4, A5;
then Lower_Support (p,T,(i + 1)) <> {} ;
then A7: HT ((Low (p,T,(i + 1))),T) in Lower_Support (p,T,(i + 1)) by A4, TERMORD:def 6;

now

assume HT ((Low (p,T,i)),T) < HT ((Low (p,T,(i + 1))),T),T ; :: thesis: contradiction
then A8: HT ((Low (p,T,i)),T) <= HT ((Low (p,T,(i + 1))),T),T by TERMORD:def 3;

now

let u9 be set ; :: thesis: ( u9 in Support (Low (p,T,i)) implies u9 in Support (Low (p,T,(i + 1))) )
assume A9: u9 in Support (Low (p,T,i)) ; :: thesis: u9 in Support (Low (p,T,(i + 1)))
then reconsider u = u9 as Element of Bags n ;
u <= HT ((Low (p,T,i)),T),T by A9, TERMORD:def 6;
hence u9 in Support (Low (p,T,(i + 1))) by A3, A6, A4, A7, A8, A9, Th24, TERMORD:8; :: thesis: verum

end;

then Support (Low (p,T,i)) c= Support (Low (p,T,(i + 1))) by TARSKI:def 3;
then (card (Support p)) + (- i) <= (card (Support p)) + (- (i + 1)) by A2, A5, NAT_1:44;
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 HT ((Low (p,T,(i + 1))),T) <= HT ((Low (p,T,i)),T),T by TERMORD:5; :: thesis: verum

end;

end;

end;

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