for n being Nat
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 ) )