theorem Th27: :: XXREAL_3:27

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