set P = Positives Q;

A: now :: thesis:

let x be object ; :: thesis:
assume x in the carrier of R ; :: thesis:
then reconsider a = x as Element of R ;

per cases by Rtot, RELAT_2:def 7;

suppose 0. R <=_ Q,a ; :: thesis:

then a in Positives Q ;
hence x in (Positives Q) \/ (- (Positives Q)) by XBOOLE_0:def 3; :: thesis:

end;

suppose a <=_ Q, 0. R ; :: thesis:

then a + (- a) <=_ Q,(0. R) + (- a) by respadd;
then 0. R <=_ Q,(0. R) + (- a) by RLVECT_1:5;
then - a in Positives Q ;
then - (- a) in - (Positives Q) ;
hence x in (Positives Q) \/ (- (Positives Q)) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

for x being object st x in (Positives Q) \/ (- (Positives Q)) holds
x in the carrier of R ;
hence Positives Q is spanning by A, TARSKI:2; :: thesis: