set P = the Preordering of R;
Positives(Poly) the Preordering of R is prepositive_cone ;
hence Polynom-Ring R is preordered ; :: thesis: verum