[:{0 },RAT+ :] c= [:{0 },REAL+ :] by ARYTM_2:1, ZFMISC_1:118;
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