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

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