theorem Th1: :: ARYTM_1:1

for x, y being Element of REAL+ st x + y = y holds
x = {}