set P = the Ordering of R;
Positives(Poly) the Ordering of R is positive_cone ;
hence Polynom-Ring R is ordered ; :: thesis: verum