let X be BCI-algebra; :: thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ; :: thesis: X is BCK-algebra
for s being Element of X holds s ` = 0. X

proof

let s be Element of X; :: thesis: s ` = 0. X
(s `) \ ((s `) \ (s \ (0. X))) = 0. X by A1;
then ((s `) \ ((s `) \ s)) \ s = s ` by Th2;
hence s ` = 0. X by Th1; :: thesis: verum

end;

hence X is BCK-algebra by Def8; :: thesis: verum