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 Th10
.= (y * z) * x by Th7
.= y * (z * x) by Th10
.= (z * x) * y by Th7 ;
hence (x * y) * z = (x * z) * y by Th7; :: thesis: verum