let X be BCI-algebra; for x, y, z being Element of X holds (x \ y) \ z = (x \ z) \ y
let x, y, z be Element of X; (x \ y) \ z = (x \ z) \ y
(x \ (x \ z)) \ z = 0. X
by Th1;
then A1:
((x \ y) \ z) \ ((x \ y) \ (x \ (x \ z))) = 0. X
by Th4;
(x \ (x \ y)) \ y = 0. X
by Th1;
then A2:
((x \ z) \ y) \ ((x \ z) \ (x \ (x \ y))) = 0. X
by Th4;
((x \ z) \ (x \ (x \ y))) \ ((x \ y) \ z) = 0. X
by Th1;
then A3:
((x \ z) \ y) \ ((x \ y) \ z) = 0. X
by A2, Th3;
((x \ y) \ (x \ (x \ z))) \ ((x \ z) \ y) = 0. X
by Th1;
then
((x \ y) \ z) \ ((x \ z) \ y) = 0. X
by A1, Th3;
hence
(x \ y) \ z = (x \ z) \ y
by A3, Def7; verum