set S = P \ {(0. R)};
A: P + P c= P by REALALG1:def 14;

now :: thesis: for s1, s2 being Element of R st s1 in P \ {(0. R)} & s2 in P \ {(0. R)} holds
s1 + s2 in P \ {(0. R)}

let s1, s2 be Element of R; :: thesis: ( s1 in P \ {(0. R)} & s2 in P \ {(0. R)} implies s1 + s2 in P \ {(0. R)} )
assume ( s1 in P \ {(0. R)} & s2 in P \ {(0. R)} ) ; :: thesis: s1 + s2 in P \ {(0. R)}
then C: ( s1 in P & not s1 in {(0. R)} & s2 in P & not s2 in {(0. R)} ) by XBOOLE_0:def 5;
then B: s1 + s2 in P + P ;

now :: thesis: not s1 + s2 in {(0. R)}

assume s1 + s2 in {(0. R)} ; :: thesis: contradiction
then s1 + s2 = 0. R by TARSKI:def 1;
then s1 = - s2 by RLVECT_1:6;
then - (- s2) in - P by C;
then s2 in P /\ (- P) by C;
hence contradiction by C, REALALG1:def 7; :: thesis: verum

end;

hence s1 + s2 in P \ {(0. R)} by A, B, XBOOLE_0:def 5; :: thesis: verum

end;

hence P ^+ is add-closed ; :: thesis: verum