( 1 in REAL+ & not 1 in {0} ) by REAL_1:1, TARSKI:def 1;
hence REAL+ \ {0} is non empty Subset of REAL+ by XBOOLE_0:def 5; :: thesis: verum