let r be Element of R; :: thesis: ( a in P & a in - P implies ( r = a iff r = - a ) )
thus ( a in P & a in - P implies ( r = a iff r = - a ) ) :: thesis: verum
proof
assume ( a in P & a in - P ) ; :: thesis: ( r = a iff r = - a )
then A: a in P /\ (- P) ;
P /\ (- P) = {(0. R)} by REALALG1:def 14;
then a = 0. R by A, TARSKI:def 1;
hence ( r = a iff r = - a ) ; :: thesis: verum
end;