let n be Nat; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for P being non empty Subset of (Polynom-Ring n,L) ex p being Polynomial of n,L st
( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for P being non empty Subset of (Polynom-Ring n,L) ex p being Polynomial of n,L st
( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for P being non empty Subset of (Polynom-Ring n,L) ex p being Polynomial of n,L st
( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )
let P be non empty Subset of (Polynom-Ring n,L); :: thesis: ex p being Polynomial of n,L st
( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )
set R = RelStr(# (Bags n),T #);
set FR = FinPoset RelStr(# (Bags n),T #);
set P' = { (Support p,T) where p is Polynomial of n,L : p in P } ;
consider p being Element of P;
reconsider p = p as Polynomial of n,L by POLYNOM1:def 27;
Support p,T in { (Support p,T) where p is Polynomial of n,L : p in P } ;
then reconsider P' = { (Support p,T) where p is Polynomial of n,L : p in P } as non empty set ;
A1: FinPoset RelStr(# (Bags n),T #) = RelStr(# (Fin the carrier of RelStr(# (Bags n),T #)),(FinOrd RelStr(# (Bags n),T #)) #) by BAGORDER:def 18;

now

let u be set ; :: thesis: ( u in P' implies u in the carrier of (FinPoset RelStr(# (Bags n),T #)) )
assume u in P' ; :: thesis: u in the carrier of (FinPoset RelStr(# (Bags n),T #))
then consider p being Polynomial of n,L such that
A2: ( u = Support p,T & p in P ) ;
thus u in the carrier of (FinPoset RelStr(# (Bags n),T #)) by A1, A2; :: thesis: verum

end;

then A3: P' c= the carrier of (FinPoset RelStr(# (Bags n),T #)) by TARSKI:def 3;
set m = MinElement P',(FinPoset RelStr(# (Bags n),T #));
FinPoset RelStr(# (Bags n),T #) is well_founded by BAGORDER:42;
then A4: ( MinElement P',(FinPoset RelStr(# (Bags n),T #)) in P' & MinElement P',(FinPoset RelStr(# (Bags n),T #)) is_minimal_wrt P',the InternalRel of (FinPoset RelStr(# (Bags n),T #)) ) by A3, BAGORDER:def 19;
then consider p being Polynomial of n,L such that
A5: ( Support p,T = MinElement P',(FinPoset RelStr(# (Bags n),T #)) & p in P ) ;
take p ; :: thesis: ( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) )

now

let q be Polynomial of n,L; :: thesis: ( q in P implies p <= q,T )
assume A6: q in P ; :: thesis: p <= q,T
set sq = Support q,T;
A7: Support q,T in P' by A6;

now

per cases ( Support p = Support q or Support p <> Support q ) ;

case Support p = Support q ; :: thesis: p <= q,T

hence p <= q,T by Th26; :: thesis: verum

end;

case Support p <> Support q ; :: thesis: p <= q,T

then not [(Support q,T),(MinElement P',(FinPoset RelStr(# (Bags n),T #)))] in the InternalRel of (FinPoset RelStr(# (Bags n),T #)) by A4, A5, A7, WAYBEL_4:def 26;
then not q <= p,T by A1, A5, Def2;
hence p <= q,T by Th28; :: thesis: verum

end;

end;

end;

hence p <= q,T ; :: thesis: verum

end;

hence ( p in P & ( for q being Polynomial of n,L st q in P holds
p <= q,T ) ) by A5; :: thesis: verum