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