let X be BCI-Algebra_with_Condition(S); :: thesis: for x, y, z being Element of X holds (x * y) * z = (x * z) * y
let x, y, z be Element of X; :: thesis: (x * y) * z = (x * z) * y
(x * y) * z = x * (y * z) by Th9
.= (y * z) * x by Th6
.= y * (z * x) by Th9
.= (z * x) * y by Th6 ;
hence (x * y) * z = (x * z) * y by Th6; :: thesis: verum