theorem :: REALALG1:42

for R being ordered domRing
for O being Ordering of R holds Positives(Poly) O is Ordering of (Polynom-Ring R) ;