now :: thesis: for e being object holds
( ( e in DEDEKIND_CUTS /\ RAT+ implies e = {} ) & ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) )
let e be object ; :: thesis: ( ( e in DEDEKIND_CUTS /\ RAT+ implies e = {} ) & ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) )
thus ( e in DEDEKIND_CUTS /\ RAT+ implies e = {} ) :: thesis: ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ )
proof
assume that
A1: e in DEDEKIND_CUTS /\ RAT+ and
A2: e <> {} ; :: thesis: contradiction
reconsider A = e as non empty Subset of RAT+ by A1, A2;
A in RAT+ by A1, XBOOLE_0:def 4;
then A3: ex s being Element of RAT+ st
( s in A & ( for r being Element of RAT+ st r in A holds
r <=' s ) ) by ARYTM_3:91;
e in DEDEKIND_CUTS by A1, XBOOLE_0:def 4;
hence contradiction by A3, Lm7; :: thesis: verum
end;
thus ( e = {} implies e in DEDEKIND_CUTS /\ RAT+ ) by Lm8, XBOOLE_0:def 4; :: thesis: verum
end;
hence DEDEKIND_CUTS /\ RAT+ = {{}} by TARSKI:def 1; :: thesis: verum