theorem Th7: :: XXREAL_3:7

for x being ExtReal holds x + (- x) = 0