let x, y be Element of REAL+ ; :: thesis: ( x + y = y implies x = {} )
reconsider o = {} as Element of REAL+ by ARYTM_2:20;
assume x + y = y ; :: thesis: x = {}
then x + y = y + o by ARYTM_2:def 8;
hence x = {} by ARYTM_2:11; :: thesis: verum