let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L holds PosetMax (Support p,T) = HT p,T
let T be connected TermOrder of n; :: thesis: for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L holds PosetMax (Support p,T) = HT p,T
let L be non trivial ZeroStr ; :: thesis: for p being non-zero Polynomial of n,L holds PosetMax (Support p,T) = HT p,T
let p be non-zero Polynomial of n,L; :: thesis: PosetMax (Support p,T) = HT p,T
set htp = HT p,T;
set R = RelStr(# (Bags n),T #);
set sp = Support p,T;
p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A1: ( HT p,T in Support p & ( for b being bag of st b in Support p holds
b <= HT p,T,T ) ) by TERMORD:def 6;

now

assume ex y being set st
( y in Support p,T & y <> HT p,T & [(HT p,T),y] in the InternalRel of RelStr(# (Bags n),T #) ) ; :: thesis: contradiction
then consider y being set such that
A2: ( y in Support p,T & y <> HT p,T & [(HT p,T),y] in the InternalRel of RelStr(# (Bags n),T #) ) ;
y is Element of Bags n by A2;
then reconsider y' = y as bag of ;
( y' <= HT p,T,T & HT p,T <= y',T ) by A2, TERMORD:def 2, TERMORD:def 6;
hence contradiction by A2, TERMORD:7; :: thesis: verum

end;

then HT p,T is_maximal_wrt Support p,T,the InternalRel of RelStr(# (Bags n),T #) by A1, WAYBEL_4:def 24;
hence PosetMax (Support p,T) = HT p,T by A1, BAGORDER:def 15; :: thesis: verum