let X be BCI-algebra; :: thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ) implies X is BCK-algebra )
assume A1: for X being BCI-algebra
for x, y being Element of X holds x \ (y \ x) = x ; :: 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 \ (0. X)) ` = 0. X by A1;
hence z ` = 0. X by Th2; :: thesis: verum
end;
hence X is BCK-algebra by Def8; :: thesis: verum