let S be Subring of R; :: thesis: S is preordered
set P = the Preordering of R;
for o being object st o in the Preordering of R /\ the carrier of S holds
o in the carrier of S by XBOOLE_0:def 4;
then reconsider M = the Preordering of R /\ the carrier of S as Subset of S by TARSKI:def 3;
M is prepositive_cone by lemsubpreord;
hence S is preordered ; :: thesis: verum