theorem Th22: :: XXREAL_3:22

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