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