:: deftheorem defines Positives(Poly) REALALG1:def 24 :
for R being preordered Ring
for P being Preordering of R holds Positives(Poly) P = { p where p is Polynomial of R : LC p in P } ;