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 1;
then Support p <> {} by POLYNOM7:1;
then A1: HT (p,T) in Support p by TERMORD:def 6;

now :: thesis: for y being set holds
( not y in Support (p,T) or not y <> HT (p,T) or not [(HT (p,T)),y] in the InternalRel of RelStr(# (Bags n),T #) )

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) and
A3: y <> HT (p,T) and
A4: [(HT (p,T)),y] in the InternalRel of RelStr(# (Bags n),T #) ;
y is Element of Bags n by A2;
then reconsider y9 = y as bag of n ;
( y9 <= HT (p,T),T & HT (p,T) <= y9,T ) by A2, A4, TERMORD:def 2, TERMORD:def 6;
hence contradiction by A3, 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 23;
hence PosetMax (Support (p,T)) = HT (p,T) by A1, BAGORDER:def 13; :: thesis: verum