let R be ordered Ring; :: thesis: for O being Ordering of R
for S being Subring of R
for Q being Subset of S st Q = O /\ the carrier of S holds
Q is positive_cone
let O be Ordering of R; :: thesis: for S being Subring of R
for Q being Subset of S st Q = O /\ the carrier of S holds
Q is positive_cone
let S be Subring of R; :: thesis: for Q being Subset of S st Q = O /\ the carrier of S holds
Q is positive_cone
let Q be Subset of S; :: thesis: ( Q = O /\ the carrier of S implies Q is positive_cone )
assume AS: Q = O /\ the carrier of S ; :: thesis: Q is positive_cone
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: for o being object st o in the carrier of S holds
o in - E

let o be object ; :: thesis: ( o in the carrier of S implies o in - E )
assume o in the carrier of S ; :: thesis: o in - E
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: verum

end;

now :: thesis: for o being object st o in - E holds
o in the carrier of S

let o be object ; :: thesis: ( o in - E implies o in the carrier of S )
assume o in - E ; :: thesis: o in the carrier of S
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: verum

end;

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

B: now :: thesis: for o being object st o in the carrier of S holds
o in Q \/ (- Q)

let o be object ; :: thesis: ( o in the carrier of S implies b₁ in Q \/ (- Q) )
assume A0: o in the carrier of S ; :: thesis: b₁ in Q \/ (- Q)
then reconsider a = o as Element of R by AS4;
A1: O is spanning ;

per cases ( a in O or a in - O ) by A1, XBOOLE_0:def 3;

suppose a in O ; :: thesis: b₁ in Q \/ (- Q)

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: verum

end;

suppose a in - O ; :: thesis: b₁ in Q \/ (- Q)

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: verum

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: verum