theorem :: REALALG1:41

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