let e be set ; :: thesis: ( e in REAL+ implies e <> RAT+ )
assume e in REAL+ ; :: thesis: e <> RAT+
then ( e in RAT+ or e in DEDEKIND_CUTS ) by XBOOLE_0:def 3;
hence e <> RAT+ by ZFMISC_1:56; :: thesis: verum