theorem Th25: :: XXREAL_3:25

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