let X be BCI-algebra; :: thesis: ( ( for X being BCI-algebra

for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) implies X is BCK-algebra )

assume A1: for X being BCI-algebra

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

for z being Element of X holds z ` = 0. X

for x, y being Element of X holds x \ (x \ y) = y \ (y \ x) ) implies X is BCK-algebra )

assume A1: for X being BCI-algebra

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

for z being Element of X holds z ` = 0. X

proof

hence
X is BCK-algebra
by Def8; :: thesis: verum
let z be Element of X; :: thesis: z ` = 0. X

(z `) ` = z \ (z \ (0. X)) by A1;

then (z `) ` = z \ z by Th2;

then ((z `) `) \ z = z ` by Def5;

hence z ` = 0. X by Th1; :: thesis: verum

end;(z `) ` = z \ (z \ (0. X)) by A1;

then (z `) ` = z \ z by Th2;

then ((z `) `) \ z = z ` by Def5;

hence z ` = 0. X by Th1; :: thesis: verum