for x, y, z being ExtReal st 0 <= x & 0 <= y & 0 <= z holds
(x + y) + z = x + (y + z)