let B be set ; :: thesis: ( B in DEDEKIND_CUTS & B <> {} implies {} in B )
assume that
A1: B in DEDEKIND_CUTS and
A2: B <> {} ; :: thesis: {} in B
reconsider B = B as non empty Subset of RAT+ by A1, A2;
ex r being Element of RAT+ st r in B by SUBSET_1:4;
hence {} in B by A1, Lm16, ARYTM_3:64; :: thesis: verum