let X be BCK-algebra; :: thesis: ( X is BCK-implicative BCK-algebra iff for x, y being Element of X holds x \ (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) = (y \ (y \ x)) \ (x \ y) ) :: thesis: ( ( for x, y being Element of X holds x \ (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) = (y \ (y \ x)) \ (x \ y)
then A2: X is commutative BCK-algebra by Th34;
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 \ y) = y \ (y \ x) by A1, Th35;
then (y \ (y \ x)) \ (x \ y) = y \ (y \ x) by A2, Def1;
hence x \ (x \ y) = (y \ (y \ x)) \ (x \ y) by A2, Def1; :: thesis: verum

end;

hence for x, y being Element of X holds x \ (x \ y) = (y \ (y \ x)) \ (x \ y) ; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

then X is BCK-positive-implicative BCK-algebra by Th28;
hence X is BCK-implicative BCK-algebra by A4, Th34; :: thesis: verum