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