set P = Positives Q;

now :: thesis: for x, y being Element of R st x in Positives Q & y in Positives Q holds
x + y in Positives Q

let x, y be Element of R; :: thesis: ( x in Positives Q & y in Positives Q implies x + y in Positives Q )
assume A0: ( x in Positives Q & y in Positives Q ) ; :: thesis: x + y in Positives Q
then consider a being Element of R such that
A1: ( x = a & 0. R <=_ Q,a ) ;
consider b being Element of R such that
A2: ( y = b & 0. R <=_ Q,b ) by A0;
(0. R) + b <=_ Q,a + b by respadd, A1;
then 0. R <=_ Q,a + b by A2, lemtrans;
hence x + y in Positives Q by A1, A2; :: thesis: verum

end;

hence Positives Q is add-closed ; :: thesis: ( Positives Q is mult-closed & Positives Q is negative-disjoint )

now :: thesis: for x, y being Element of R st x in Positives Q & y in Positives Q holds
x * y in Positives Q

let x, y be Element of R; :: thesis: ( x in Positives Q & y in Positives Q implies x * y in Positives Q )
assume A0: ( x in Positives Q & y in Positives Q ) ; :: thesis: x * y in Positives Q
then consider a being Element of R such that
A1: ( x = a & 0. R <=_ Q,a ) ;
consider b being Element of R such that
A2: ( y = b & 0. R <=_ Q,b ) by A0;
(0. R) * b <=_ Q,a * b by respmult, A1, A2;
hence x * y in Positives Q by A1, A2; :: thesis: verum

end;

hence Positives Q is mult-closed ; :: thesis: Positives Q is negative-disjoint

A: now :: thesis: for x being object st x in (Positives Q) /\ (- (Positives Q)) holds
x in {(0. R)}

let x be object ; :: thesis: ( x in (Positives Q) /\ (- (Positives Q)) implies x in {(0. R)} )
assume x in (Positives Q) /\ (- (Positives Q)) ; :: thesis: x in {(0. R)}
then A0: ( x in Positives Q & x in - (Positives Q) ) by XBOOLE_0:def 4;
consider a being Element of R such that
A1: ( x = a & 0. R <=_ Q,a ) by A0;
consider b being Element of R such that
A2: ( x = - b & b in Positives Q ) by A0;
consider c being Element of R such that
A3: ( c = b & 0. R <=_ Q,c ) by A2;
a + (0. R) <=_ Q,a + (- a) by A3, respadd, A1, A2;
then a <=_ Q, 0. R by RLVECT_1:5;
then a = 0. R by A1, lemanti;
hence x in {(0. R)} by A1, TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for x being object st x in {(0. R)} holds
x in (Positives Q) /\ (- (Positives Q))

let x be object ; :: thesis: ( x in {(0. R)} implies x in (Positives Q) /\ (- (Positives Q)) )
assume C: x in {(0. R)} ; :: thesis: x in (Positives Q) /\ (- (Positives Q))
then A: x = 0. R by TARSKI:def 1;
reconsider a = x as Element of R by C;
a <=_ Q,a by defstr, RELAT_2:def 1;
then B: a in Positives Q by A;
- a = a by A;
then a in - (Positives Q) by B;
hence x in (Positives Q) /\ (- (Positives Q)) by B, XBOOLE_0:def 4; :: thesis: verum

end;

hence Positives Q is negative-disjoint by A, TARSKI:2; :: thesis: verum