theorem Th30: :: XXREAL_3:30

for x, y, z being ExtReal st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds
(x + y) - z = x + (y - z)