A: P + P c= P by REALALG1:def 14;
D: ( a in P \ {(0. R)} & b in P \ {(0. R)} ) by REALALG2:def 8;
then C: ( a in P & b in P ) by XBOOLE_0:def 5;
then B: a + b in P + P ;

now :: thesis: not a + b = 0. R

assume a + b = 0. R ; :: thesis: contradiction
then a = - b by RLVECT_1:6;
then - (- b) in - P by C;
then b in P /\ (- P) by C;
then b in {(0. R)} by REALALG1:def 7;
hence contradiction by D, XBOOLE_0:def 5; :: thesis: verum

end;

then not a + b in {(0. R)} by TARSKI:def 1;
then a + b in P \ {(0. R)} by A, B, XBOOLE_0:def 5;
hence a + b is P -positive by REALALG2:def 8; :: thesis: verum