let x, y be Element of REAL+ ; :: thesis: ( x + y = x implies y = {} )
assume that
A1: x + y = x and
A2: y <> {} ; :: thesis: contradiction
A3: x <> {} by A1, A2, Th5;
then A4: DEDEKIND_CUT x <> {} by Lm10;
DEDEKIND_CUT x = DEDEKIND_CUT (GLUED ((DEDEKIND_CUT x) + (DEDEKIND_CUT y))) by A1, A2, A3, Def8
.= (DEDEKIND_CUT x) + (DEDEKIND_CUT y) by Lm12 ;
then DEDEKIND_CUT y = {} by A4, Lm34;
hence contradiction by A2, Lm10; :: thesis: verum