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