let X be non empty BCIStr_0 ; :: thesis: ( X is BCK-implicative 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)) \ (x \ y) ) )
thus ( X is BCK-implicative 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)) \ (x \ y) ) ) :: thesis: ( ( for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ) 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 \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) )
let x, y, z be Element of X; :: thesis: ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) )
A2: x \ ((0. X) \ y) = x \ (y ` )
.= x \ (0. X) by A1, BCIALG_1:def 8
.= x by A1, BCIALG_1:2 ;
A3: X is commutative BCK-algebra by A1, Th34;
((y \ z) \ (y \ x)) \ (x \ y) = ((y \ z) \ (x \ y)) \ (y \ x) by A1, BCIALG_1:7
.= ((y \ (x \ y)) \ z) \ (y \ x) by A1, BCIALG_1:7
.= (y \ z) \ (y \ x) by A1, Def12
.= (y \ (y \ x)) \ z by A1, BCIALG_1:7
.= (x \ (x \ y)) \ z by A3, Def1
.= (x \ z) \ (x \ y) by A1, BCIALG_1:7 ;
hence ( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) by A2; :: thesis: verum

end;

assume A4: for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = ((y \ z) \ (y \ x)) \ (x \ y) ) ; :: thesis: X is BCK-implicative BCK-algebra
A5: 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 A4;
hence x \ (0. X) = x ; :: thesis: verum

end;

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

end;

A7: for y being Element of X holds y \ y = 0. X

proof

let y be Element of X; :: thesis: y \ y = 0. X
(0. X) \ ((0. X) \ y) = (y \ (y \ (0. X))) \ ((0. X) \ y) by A6
.= (y \ y) \ ((0. X) \ y) by A5
.= y \ y by A4 ;
hence y \ y = 0. X by A4; :: thesis: verum

end;

A8: 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)) \ (0. X) by A4
.= (y \ (0. X)) \ (0. X) by A5 ;
then x \ (0. X) = (y \ (0. X)) \ (0. X) by A5
.= y \ (0. X) by A5 ;
hence x = y \ (0. X) by A5
.= y by A5 ;
:: thesis: verum

end;

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

then A14: X is commutative BCK-algebra by A4, Th6;
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) = y \ (y \ x) by A14, Def1;
hence (x \ (x \ y)) \ (x \ y) = y \ (y \ x) by A6; :: thesis: verum

end;

hence X is BCK-implicative BCK-algebra by A4, A12, Th6, Th35; :: thesis: verum