let x be Element of REAL+ ; :: thesis: ( DEDEKIND_CUT x = {} iff x = {} )
A1: for e being object holds not e in { s where s is Element of RAT+ : s < {} }

proof

given e being object such that A2: e in { s where s is Element of RAT+ : s < {} } ; :: thesis: contradiction
ex s being Element of RAT+ st
( s = e & s < {} ) by A2;
hence contradiction by ARYTM_3:64; :: thesis: verum

end;

thus ( DEDEKIND_CUT x = {} implies x = {} ) :: thesis: ( x = {} implies DEDEKIND_CUT x = {} )

proof

assume A3: DEDEKIND_CUT x = {} ; :: thesis: x = {}

per cases ( x in RAT+ or not x in RAT+ ) ;

suppose A4: x in RAT+ ; :: thesis: x = {}

assume A5: x <> {} ; :: thesis: contradiction
consider r being Element of RAT+ such that
A6: x = r and
A7: DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } by A4, Def3;
{} <=' r by ARYTM_3:64;
then {} < r by A6, A5, ARYTM_3:68;
then {} in DEDEKIND_CUT x by A7;
hence contradiction by A3; :: thesis: verum

end;

suppose not x in RAT+ ; :: thesis: x = {}

hence x = {} by A3, Def3; :: thesis: verum

end;

end;

end;

assume x = {} ; :: thesis: DEDEKIND_CUT x = {}
then ex r being Element of RAT+ st
( {} = r & DEDEKIND_CUT x = { s where s is Element of RAT+ : s < r } ) by Def3;
hence DEDEKIND_CUT x = {} by A1, XBOOLE_0:def 1; :: thesis: verum