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

proof

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

end;

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

proof

let x, y be Element of X; :: thesis: x \ (x \ y) = y \ (y \ x)
(x \ (0. X)) \ (x \ y) = (y \ (0. X)) \ ((y \ x) \ (0. X)) by A4;
then (x \ (0. X)) \ (x \ y) = y \ ((y \ x) \ (0. X)) by BCIALG_1:2;
then (x \ (0. X)) \ (x \ y) = y \ (y \ x) by BCIALG_1:2;
hence x \ (x \ y) = y \ (y \ x) by BCIALG_1:2; :: thesis: verum

end;

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

proof

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

end;

then for x, y being Element of X holds (x \ (x \ y)) \ (x \ y) = y \ (y \ x) ;
hence X is BCK-implicative BCK-algebra by Th35; :: thesis: verum