set P = the Preordering of R;
take OrdRel the Preordering of R ; :: thesis: ( OrdRel the Preordering of R is strongly_reflexive & OrdRel the Preordering of R is antisymmetric & OrdRel the Preordering of R is transitive & OrdRel the Preordering of R is respecting_addition & OrdRel the Preordering of R is respecting_multiplication )
thus ( OrdRel the Preordering of R is strongly_reflexive & OrdRel the Preordering of R is antisymmetric & OrdRel the Preordering of R is transitive & OrdRel the Preordering of R is respecting_addition & OrdRel the Preordering of R is respecting_multiplication ) ; :: thesis: verum