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