RAT+ c= RAT+ \/ [:{0 },RAT+ :] by XBOOLE_1:7;
hence RAT+ c= RAT by ARYTM_3:68, ZFMISC_1:40; :: thesis: verum