theorem Th6: :: ARYTM_2:6

for x, y, z being Element of REAL+ holds x + (y + z) = (x + y) + z