REAL+ c= REAL+ \/ [:{0 },REAL+ :] by XBOOLE_1:7;
hence REAL+ c= REAL by ARYTM_2:3, ZFMISC_1:40; :: thesis: verum