theorem Th1: :: FVALUAT1:1

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