theorem :: REALALG1:43

for R being preordered domRing
for P being Preordering of R holds LowPositives(Poly) P is Preordering of (Polynom-Ring R) ;