take - (1. R) ; :: thesis: - (1. R) is P -negative
- (- (1. R)) <> - (0. R) ;
then ( 1. R in P & - (1. R) <> 0. R ) by REALALG1:25;
then ( - (1. R) in - P & not - (1. R) in {(0. R)} ) by TARSKI:def 1;
hence - (1. R) is P -negative by XBOOLE_0:def 5; :: thesis: verum