let X be non empty BCIStr_0 ; :: thesis: ( X is commutative BCK-algebra iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) )
thus ( X is commutative BCK-algebra implies for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) :: thesis: ( ( for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ) implies X is commutative BCK-algebra )

proof

assume A1: X is commutative BCK-algebra ; :: thesis: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) )
let x, y, z be Element of X; :: thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) )
A2: (0. X) \ y = y `
.= 0. X by A1, BCIALG_1:def 8 ;
(x \ (x \ y)) \ z = (y \ (y \ x)) \ z by A1, Def1;
then (x \ z) \ (x \ y) = (y \ (y \ x)) \ z by A1, BCIALG_1:7
.= (y \ z) \ (y \ x) by A1, BCIALG_1:7 ;
hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) by A1, A2, BCIALG_1:2; :: thesis: verum

end;

assume A3: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) ) ; :: thesis: X is commutative BCK-algebra
A4: for x, y being Element of X holds x \ (0. X) = x

proof

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

end;

A5: for x being Element of X holds x \ x = 0. X

proof

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

end;

A6: for x, y being Element of X st x \ y = 0. X & y \ x = 0. X holds
x = y

proof

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

end;

A7: 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 \ (x \ y) = (x \ ((0. X) \ y)) \ (x \ y) by A3
.= (y \ ((0. X) \ y)) \ (y \ x) by A3
.= y \ (y \ x) by A3 ;
hence x \ (x \ y) = y \ (y \ x) ; :: thesis: verum

end;

A8: for x being Element of X holds (0. X) \ x = 0. X

proof

let x be Element of X; :: thesis: (0. X) \ x = 0. X
0. X = ((0. X) \ x) \ ((0. X) \ x) by A5
.= (0. X) \ x by A3 ;
hence (0. X) \ x = 0. X ; :: thesis: verum

end;

A9: for x, y, z being Element of X holds ((x \ y) \ (x \ z)) \ (z \ y) = 0. X

proof

let x, y, z be Element of X; :: thesis: ((x \ y) \ (x \ z)) \ (z \ y) = 0. X
((x \ y) \ (x \ z)) \ (z \ y) = ((z \ y) \ (z \ x)) \ (z \ y) by A3
.= ((z \ y) \ (z \ x)) \ ((z \ y) \ (0. X)) by A4
.= ((0. X) \ (z \ x)) \ ((0. X) \ (z \ y)) by A3
.= (0. X) \ ((0. X) \ (z \ y)) by A8
.= 0. X by A8 ;
hence ((x \ y) \ (x \ z)) \ (z \ y) = 0. X ; :: thesis: verum

end;

A10: for x, y being Element of X holds (x \ (x \ y)) \ y = 0. X

proof

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

end;

A11: for x being Element of X holds x ` = 0. X by A8;
( X is being_I & X is being_BCI-4 ) by A5, A6, BCIALG_1:def 5, BCIALG_1:def 7;
hence X is commutative BCK-algebra by A7, A9, A10, A11, Def1, BCIALG_1:1, BCIALG_1:def 8; :: thesis: verum