theorem Th5: :: ARYTM_2:5

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