:: deftheorem defines LowPositives(Poly) REALALG1:def 25 :
for R being preordered Ring
for P being Preordering of R holds LowPositives(Poly) P = { p where p is Polynomial of R : p . (min* { i where i is Nat : p . i <> 0. R } ) in P } ;