theorem Th11: :: BCIALG_4:12

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