let R be preordered Ring; :: thesis: for P being Preordering of R
for S being Subring of R holds P /\ the carrier of S is Preordering of S
let O be Preordering of R; :: thesis: for S being Subring of R holds O /\ the carrier of S is Preordering of S
let S be Subring of R; :: thesis: O /\ the carrier of S is Preordering 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 prepositive_cone by lemsubpreord;
hence O /\ the carrier of S is Preordering of S ; :: thesis: verum