let B be set ; :: thesis: ( B in DEDEKIND_CUTS implies ex r being Element of RAT+ st not r in B )
assume A1: B in DEDEKIND_CUTS ; :: thesis: not for r being Element of RAT+ holds r in B
then reconsider B = B as Subset of RAT+ ;
B <> RAT+ by A1, ZFMISC_1:56;
hence not for r being Element of RAT+ holds r in B by SUBSET_1:28; :: thesis: verum