theorem Th9: :: BCIALG_4:10

for X being BCI-Algebra_with_Condition(S)
for x, y, z being Element of X holds (x * y) * z = x * (y * z)