set P = Positives Q;

A: now :: thesis: for x being object st x in the carrier of R holds
x in (Positives Q) \/ (- (Positives Q))

let x be object ; :: thesis: ( x in the carrier of R implies b₁ in (Positives Q) \/ (- (Positives Q)) )
assume x in the carrier of R ; :: thesis: b₁ in (Positives Q) \/ (- (Positives Q))
then reconsider a = x as Element of R ;

per cases ( 0. R <=_ Q,a or a <=_ Q, 0. R ) by Rtot, RELAT_2:def 7;

suppose 0. R <=_ Q,a ; :: thesis: b₁ in (Positives Q) \/ (- (Positives Q))

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

end;

suppose a <=_ Q, 0. R ; :: thesis: b₁ in (Positives Q) \/ (- (Positives Q))

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

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