assume A2: X is BCK-implicative ; :: thesis: for x, y being Element of X holds (a \ y) \ ((a \ y) \ x) = x \ y
let x, y be Element of X; :: thesis: (a \ y) \ ((a \ y) \ x) = x \ y
X is involutory by A2, Th37;
then A3: x \ (a \ y) = y \ (a \ x) by A1, Th23;
A4: (a \ y) \ ((a \ y) \ x) = x \ (x \ (a \ y)) by Def1;
(y \ (a \ x)) \ y = (y \ y) \ (a \ x) by BCIALG_1:7
.= (a \ x) ` by BCIALG_1:def 5
.= 0. X by BCIALG_1:def 8 ;
then x \ (a \ y) <= y by A3;
then x \ y <= (a \ y) \ ((a \ y) \ x) by A4, BCIALG_1:5;
then A5: (x \ y) \ ((a \ y) \ ((a \ y) \ x)) = 0. X ;
X is BCK-positive-implicative BCK-algebra by A2, Th34;
then a \ y = (a \ y) \ y by Th28;
then ((a \ y) \ ((a \ y) \ x)) \ (x \ y) = 0. X by BCIALG_1:1;
hence (a \ y) \ ((a \ y) \ x) = x \ y by A5, BCIALG_1:def 7; :: thesis: verum

let x be Element of X; :: thesis: (a \ x) \ ((a \ x) \ x) = 0. X
(a \ x) \ ((a \ x) \ x) = x \ x by A6;
hence (a \ x) \ ((a \ x) \ x) = 0. X by BCIALG_1:def 5; :: thesis: verum