[:{0},RAT+:] c= [:{0},REAL+:] by ARYTM_2:1, ZFMISC_1:95;
then RAT+ \/ [:{0},RAT+:] c= REAL+ \/ [:{0},REAL+:] by ARYTM_2:1, XBOOLE_1:13;
hence RAT c= REAL by XBOOLE_1:33; :: thesis: verum