theorem Th9: :: XXREAL_3:9

for x, y being ExtReal holds - (x + y) = (- x) + (- y)