let R be ordered Ring; :: thesis:
let O be Ordering of R; :: thesis:
let S be Subring of R; :: thesis:
let Q be Subset of S; :: thesis:
assume AS: Q = O /\ the carrier of S ; :: thesis:
then AS1: Q is prepositive_cone by lemsubpreord;
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
reconsider E = the carrier of S as Subset of R by C0SP1:def 3;

AS3: now :: thesis:

let o be object ; :: thesis:
assume o in the carrier of S ; :: thesis:
then reconsider a = o as Element of S ;
reconsider b = - a as Element of R by AS4;
- b = - (- a) by lemminus
.= o ;
hence o in - E ; :: thesis:

end;

now :: thesis:

let o be object ; :: thesis:
assume o in - E ; :: thesis:
then consider a being Element of R such that
B: ( - a = o & a in E ) ;
reconsider b = a as Element of S by B;
- a = - b by lemminus;
hence o in the carrier of S by B; :: thesis:

end;

then AS2: the carrier of S = - E by AS3, TARSKI:2;

B: now :: thesis:

let o be object ; :: thesis:
assume A0: o in the carrier of S ; :: thesis:
then reconsider a = o as Element of R by AS4;
A1: O is spanning ;

per cases by A1, XBOOLE_0:def 3;

suppose a in O ; :: thesis:

then a in O /\ the carrier of S by A0, XBOOLE_0:def 4;
hence o in Q \/ (- Q) by AS, XBOOLE_0:def 3; :: thesis:

end;

suppose a in - O ; :: thesis:

then a in (- O) /\ (- E) by AS2, A0, XBOOLE_0:def 4;
then o in - (O /\ the carrier of S) by min1;
then o in - Q by AS, lemminus1;
hence o in Q \/ (- Q) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

for o being object st o in Q \/ (- Q) holds
o in the carrier of S ;
hence Q is positive_cone by AS1, B, TARSKI:2; :: thesis: