let R be preordered Ring; :: thesis: for P being Preordering of R
for S being Subring of R
for Q being Subset of S st Q = P /\ the carrier of S holds
Q is prepositive_cone
let P be Preordering of R; :: thesis: for S being Subring of R
for Q being Subset of S st Q = P /\ the carrier of S holds
Q is prepositive_cone
let S be Subring of R; :: thesis: for Q being Subset of S st Q = P /\ the carrier of S holds
Q is prepositive_cone
let Q be Subset of S; :: thesis: ( Q = P /\ the carrier of S implies Q is prepositive_cone )
assume AS: Q = P /\ the carrier of S ; :: thesis: Q is prepositive_cone

now :: thesis: for o being object st o in Q holds
o in the carrier of R

let o be object ; :: thesis: ( o in Q implies o in the carrier of R )
assume A: o in Q ; :: thesis: o in the carrier of R
the carrier of S c= the carrier of R by C0SP1:def 3;
hence o in the carrier of R by A; :: thesis: verum

end;

then reconsider Q1 = Q as Subset of R by TARSKI:def 3;
AS1: - Q1 = - Q by lemminus1;
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;
A: Q + Q c= Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q + Q or x in Q )
assume x in Q + Q ; :: thesis: x in Q
then x in { (a + b) where a, b is Element of S : ( a in Q & b in Q ) } by IDEAL_1:def 19;
then consider a, b being Element of S such that
A1: ( x = a + b & a in Q & b in Q ) ;
A2: ( a in P & b in P ) by A1, AS, XBOOLE_0:def 4;
reconsider a1 = a, b1 = b as Element of R by A1, AS;
a1 + b1 in { (u + v) where u, v is Element of R : ( u in P & v in P ) } by A2;
then A3: a1 + b1 in P + P by IDEAL_1:def 19;
A4: P + P c= P by defppc;
dom the addF of S = [: the carrier of S, the carrier of S:] by FUNCT_2:def 1;
then A6: [a,b] in dom the addF of S ;
a1 + b1 = ( the addF of R || the carrier of S) . (a,b) by A6, FUNCT_1:49
.= a + b by C0SP1:def 3 ;
hence x in Q by A1, AS, A4, A3, XBOOLE_0:def 4; :: thesis: verum

end;

B: Q * Q c= Q

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q * Q or x in Q )
assume x in Q * Q ; :: thesis: x in Q
then consider a, b being Element of S such that
B1: ( x = a * b & a in Q & b in Q ) ;
B2: ( a in P & b in P ) by B1, AS, XBOOLE_0:def 4;
reconsider a1 = a, b1 = b as Element of R by B1, AS;
B3: a1 * b1 in P * P by B2;
B4: P * P c= P by defppc;
dom the multF of S = [: the carrier of S, the carrier of S:] by FUNCT_2:def 1;
then B6: [a,b] in dom the multF of S ;
a1 * b1 = ( the multF of R || the carrier of S) . (a,b) by B6, FUNCT_1:49
.= a * b by C0SP1:def 3 ;
hence x in Q by B1, AS, B4, B3, XBOOLE_0:def 4; :: thesis: verum

end;

C1: now :: thesis: for o being object st o in Q /\ (- Q) holds
o in {(0. S)}

let o be object ; :: thesis: ( o in Q /\ (- Q) implies o in {(0. S)} )
assume o in Q /\ (- Q) ; :: thesis: o in {(0. S)}
then C3: ( o in Q & o in - Q ) by XBOOLE_0:def 4;
then o in - (P /\ the carrier of S) by AS, lemminus1;
then o in (- P) /\ (- E) by min1;
then ( o in P & o in - P ) by C3, AS, XBOOLE_0:def 4;
then C2: o in P /\ (- P) by XBOOLE_0:def 4;
P /\ (- P) = {(0. R)} by defppc;
hence o in {(0. S)} by C2, C0SP1:def 3; :: thesis: verum

end;

C: now :: thesis: for o being object st o in {(0. S)} holds
o in Q /\ (- Q)

let o be object ; :: thesis: ( o in {(0. S)} implies o in Q /\ (- Q) )
assume CC: o in {(0. S)} ; :: thesis: o in Q /\ (- Q)
then o = 0. S by TARSKI:def 1
.= 0. R by C0SP1:def 3 ;
then o in {(0. R)} by TARSKI:def 1;
then o in P /\ (- P) by defppc;
then C2: ( o in P & o in - P ) by XBOOLE_0:def 4;
then C5: o in Q by CC, AS, XBOOLE_0:def 4;
o in (- P) /\ (- E) by AS2, C2, CC, XBOOLE_0:def 4;
then o in - (P /\ the carrier of S) by min1;
hence o in Q /\ (- Q) by AS1, AS, C5, XBOOLE_0:def 4; :: thesis: verum

end;

Q: SQ S c= SQ R by SQsub;
SQ R c= P by defppc;
then SQ S c= P by Q;
then SQ S c= P /\ the carrier of S by XBOOLE_0:def 4;
hence Q is prepositive_cone by A, B, C, C1, AS, TARSKI:2; :: thesis: verum