theorem Th10: :: BCIALG_4:11

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