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

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

assume A1: for X being BCI-algebra

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

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

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

assume A1: for X being BCI-algebra

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

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

proof

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

(s `) \ s = (s `) \ (s \ s) by A1;

then (s `) \ s = (s `) \ (0. X) by Def5;

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

then (s `) \ ((s `) \ s) = 0. X by Def5;

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

end;(s `) \ s = (s `) \ (s \ s) by A1;

then (s `) \ s = (s `) \ (0. X) by Def5;

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

then (s `) \ ((s `) \ s) = 0. X by Def5;

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