let X be BCK-algebra; :: thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) )
thus ( X is BCK-implicative BCK-algebra implies for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) :: thesis: ( ( for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ) implies X is BCK-implicative BCK-algebra )

proof

assume A1: X is BCK-implicative BCK-algebra ; :: thesis: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y)))
let x, y be Element of X; :: thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y)))
X is commutative BCK-algebra by A1, Th34;
then y \ (y \ (x \ (x \ y))) = y \ (y \ (y \ (y \ x))) by Def1
.= y \ (y \ x) by BCIALG_1:8 ;
hence (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A1, Th35; :: thesis: verum

end;

assume A2: for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) ; :: thesis: X is BCK-implicative BCK-algebra
A3: for x, y being Element of X holds (x \ y) \ y = x \ y

proof

let x, y be Element of X; :: thesis: (x \ y) \ y = x \ y
A4: (x \ y) \ ((x \ y) \ (x \ (x \ (x \ y)))) = (x \ y) \ ((x \ y) \ (x \ y)) by BCIALG_1:8
.= (x \ y) \ (0. X) by BCIALG_1:def 5
.= x \ y by BCIALG_1:2 ;
(x \ (x \ (x \ y))) \ (x \ (x \ y)) = (x \ y) \ (x \ (x \ y)) by BCIALG_1:8
.= (x \ (x \ (x \ y))) \ y by BCIALG_1:7
.= (x \ y) \ y by BCIALG_1:8 ;
hence (x \ y) \ y = x \ y by A2, A4; :: thesis: verum

end;

for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))

proof

let x, y be Element of X; :: thesis: x \ (x \ y) = y \ (y \ (x \ (x \ y)))
x \ (x \ y) = (x \ (x \ y)) \ (x \ y) by A3;
hence x \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2; :: thesis: verum

end;

then A5: X is commutative BCK-algebra by Th4;
for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x)

proof

let x, y be Element of X; :: thesis: (x \ (x \ y)) \ (x \ y) = y \ (y \ x)
(x \ (x \ y)) \ (x \ y) = y \ (y \ (x \ (x \ y))) by A2
.= y \ (y \ (y \ (y \ x))) by A5, Def1 ;
hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by BCIALG_1:8; :: thesis: verum

end;

hence X is BCK-implicative BCK-algebra by Th35; :: thesis: verum