REAL \ IRRAT = REAL /\ RAT by BORSUK_5:def 1, XBOOLE_1:48;
hence RAT = REAL \ IRRAT by NUMBERS:12, XBOOLE_1:28; :: thesis: verum