theorem :: XXREAL_3:8

for x, y being ExtReal st x + y = 0 holds
x = - y