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 } ;
set p = the Element of P;
reconsider p = the Element of P as Polynomial of n,L by POLYNOM1:def 11;
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 16;

now :: thesis: for u being object st u in P9 holds
u in the carrier of (FinPoset RelStr(# (Bags n),T #))

let u be object ; :: 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:41;
then MinElement (P9,(FinPoset RelStr(# (Bags n),T #))) in P9 by A2, BAGORDER:def 17;
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 17;

now :: thesis: for q being Polynomial of n,L st q in P holds
p <= q,T

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 :: thesis: ( ( Support p = Support q & p <= q,T ) or ( Support p <> Support q & p <= q,T ) )

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 25;
then not q <= p,T by A1, A4;
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