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