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

proof

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

end;

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