let X be BCI-algebra; :: 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 \ (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; :: thesis: verum

let x, y, z be Element of X; :: thesis: (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; :: thesis: verum