theorem Th2: :: FVALUAT1:2

for x being ExtReal st x + x = 0 holds
x = 0