let x be Element of REAL+ ; :: thesis: ( DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } implies x in RAT+ )
assume A1: DEDEKIND_CUT x in { { s where s is Element of RAT+ : s < t } where t is Element of RAT+ : t <> {} } ; :: thesis: x in RAT+
assume not x in RAT+ ; :: thesis: contradiction
then DEDEKIND_CUT x = x by Def3;
hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum