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