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