let x, y be Element of REAL+ ; :: thesis: ( x + y = {} implies x = {} )
assume A1: x + y = {} ; :: thesis: x = {}

per cases ( y = {} or y <> {} ) ;

suppose y = {} ; :: thesis: x = {}

hence x = {} by A1, Def8; :: thesis: verum

end;

suppose A2: y <> {} ; :: thesis: x = {}

assume A3: x <> {} ; :: thesis: contradiction
then A4: GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y)) = {} by A1, A2, Def8;
DEDEKIND_CUT x <> {} by A3, Lm10;
then consider r0 being Element of RAT+ such that
A5: r0 in DEDEKIND_CUT x by SUBSET_1:10;
DEDEKIND_CUT y <> {} by A2, Lm10;
then consider s0 being Element of RAT+ such that
A6: s0 in DEDEKIND_CUT y by SUBSET_1:10;
r0 + s0 in { (r + s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } by A5, A6;
hence contradiction by A4, Lm11; :: thesis: verum

end;

end;