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

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