let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds HM p,T <= p,T
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds HM p,T <= p,T
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds HM p,T <= p,T
let p' be Polynomial of n,L; :: thesis: HM p',T <= p',T

per cases ( p' = 0_ n,L or p' <> 0_ n,L ) ;

suppose A1: p' = 0_ n,L ; :: thesis: HM p',T <= p',T

now

assume Support (HM p',T) <> {} ; :: thesis: contradiction
then consider u being bag of such that
A2: Support (HM p',T) = {u} by POLYNOM7:6;
A3: u in Support (HM p',T) by A2, TARSKI:def 1;

now

let v be bag of ; :: thesis: ( v in Support (HM p',T) implies v <= u,T )
assume v in Support (HM p',T) ; :: thesis: v <= u,T
then u = v by A2, TARSKI:def 1;
hence v <= u,T by TERMORD:6; :: thesis: verum

end;

then A4: HT (HM p',T),T = u by A3, TERMORD:def 6;
0. L = p' . (HT p',T) by A1, POLYNOM1:81
.= HC p',T by TERMORD:def 7
.= HC (HM p',T),T by TERMORD:27
.= (HM p',T) . u by A4, TERMORD:def 7 ;
hence contradiction by A3, POLYNOM1:def 9; :: thesis: verum

end;

then HM p',T = 0_ n,L by POLYNOM7:1;
hence HM p',T <= p',T by A1, Th25; :: thesis: verum

end;

suppose p' <> 0_ n,L ; :: thesis: HM p',T <= p',T

then reconsider p = p' as non-zero Polynomial of n,L by POLYNOM7:def 2;
set hmp = HM p,T;
set R = RelStr(# (Bags n),T #);
set x = Support (HM p,T),T;
set y = Support p,T;
A5: PosetMax (Support (HM p,T),T) = HT (HM p,T),T by Th24
.= HT p,T by TERMORD:26 ;
then A6: PosetMax (Support (HM p,T),T) = PosetMax (Support p,T) by Th24;
A7: p <> 0_ n,L by POLYNOM7:def 2;
then A8: Support p <> {} by POLYNOM7:1;
(HM p,T) . (HT p,T) = p . (HT p,T) by TERMORD:18
.= HC p,T by TERMORD:def 7 ;
then A9: (HM p,T) . (HT p,T) <> 0. L by A7, TERMORD:17;
then A10: HT p,T in Support (HM p,T) by POLYNOM1:def 9;
A11: Support (HM p,T),T <> {} by A9, POLYNOM1:def 9;
A12: ( (Support (HM p,T),T) \ {(PosetMax (Support (HM p,T),T))} is Element of Fin the carrier of RelStr(# (Bags n),T #) & (Support p,T) \ {(PosetMax (Support p,T))} is Element of Fin the carrier of RelStr(# (Bags n),T #) ) by BAGORDER:38;
Support (HM p,T) = {(HT p,T)} by A10, TERMORD:21;
then (Support (HM p,T),T) \ {(PosetMax (Support (HM p,T),T))} = {} by A5, XBOOLE_1:37;
then [((Support (HM p,T),T) \ {(PosetMax (Support (HM p,T),T))}),((Support p,T) \ {(PosetMax (Support p,T))})] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A12, BAGORDER:36;
then [(Support (HM p,T),T),(Support p,T)] in union (rng (FinOrd-Approx RelStr(# (Bags n),T #))) by A6, A8, A11, BAGORDER:36;
then [(Support (HM p,T),T),(Support p,T)] in FinOrd RelStr(# (Bags n),T #) by BAGORDER:def 17;
hence HM p',T <= p',T by Def2; :: thesis: verum

end;

end;