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 P9 = { (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 P9 = { (Support p,T) where p is Polynomial of n,L : p in P } as non empty set ;
set R = RelStr(# (Bags n),T #);
set FR = FinPoset RelStr(# (Bags n),T #);
set m = MinElement P9,(FinPoset RelStr(# (Bags n),T #));
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 P9 implies u in the carrier of (FinPoset RelStr(# (Bags n),T #)) )
assume u in P9 ; :: thesis: u in the carrier of (FinPoset RelStr(# (Bags n),T #))
then ex p being Polynomial of n,L st
( u = Support p,T & p in P ) ;
hence u in the carrier of (FinPoset RelStr(# (Bags n),T #)) by A1; :: thesis: verum

end;

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

now

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

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 P9,(FinPoset RelStr(# (Bags n),T #)))] in the InternalRel of (FinPoset RelStr(# (Bags n),T #)) by A6, A4, A7, WAYBEL_4:def 26;
then not q <= p,T by A1, A4, 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