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