theorem :: REALALG1:44

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