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