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