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