theorem Th29: :: XXREAL_3:29

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