1. R in P by REALALG1:25;
then A: - (1. R) in - P ;
not - (1. R) in {(0. R)} by TARSKI:def 1;
hence not P ^- is empty by A, XBOOLE_0:def 5; :: thesis: verum