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