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 )
assume A1: i < card (Support p) ; :: thesis: HT (Low p,T,(i + 1)),T <= HT (Low p,T,i),T,T
then A2: i + 1 <= card (Support p) by NAT_1:13;
set li = Low p,T,i;
set li1 = Low p,T,(i + 1);
A3: Support (Low p,T,i) c= Support p by A1, Th26;
A4: Support (Low p,T,i) = Lower_Support p,T,i by A1, Lm3;
A5: Support (Low p,T,(i + 1)) = Lower_Support p,T,(i + 1) by A2, Lm3;
A6: card (Support (Low p,T,i)) = (card (Support p)) - i by A1, A4, Th24;
A7: card (Support (Low p,T,(i + 1))) = (card (Support p)) - (i + 1) by A2, A5, Th24;

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 A5, Th24
.= 0 ;
then Support (Low p,T,(i + 1)), 0 are_equipotent by CARD_1:def 5;
then Support (Low p,T,(i + 1)) = {} by CARD_1:46;
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 A5, A7;
then Lower_Support p,T,(i + 1) <> {} ;
then A8: HT (Low p,T,(i + 1)),T in Lower_Support p,T,(i + 1) by A5, TERMORD:def 6;

now

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

now

let u' be set ; :: thesis: ( u' in Support (Low p,T,i) implies u' in Support (Low p,T,(i + 1)) )
assume A10: u' in Support (Low p,T,i) ; :: thesis: u' in Support (Low p,T,(i + 1))
then reconsider u = u' as Element of Bags n ;
u <= HT (Low p,T,i),T,T by A10, TERMORD:def 6;
then u <= HT (Low p,T,(i + 1)),T,T by A9, TERMORD:8;
hence u' in Support (Low p,T,(i + 1)) by A2, A3, A5, A8, A10, Th24; :: 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 A6, A7, 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