let X be BCI-algebra; :: thesis: ( X is being_K iff X is BCK-algebra )
thus ( X is being_K implies X is BCK-algebra ) :: thesis: ( X is BCK-algebra implies X is being_K )

proof

assume A1: X is being_K ; :: thesis: X is BCK-algebra

now :: thesis: for s being Element of X holds s ` = 0. X

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

end;

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

end;

assume A2: X is BCK-algebra ; :: thesis: X is being_K
let x, y be Element of X; :: according to BCIALG_1:def 6 :: thesis: (x \ y) \ x = 0. X
y ` = 0. X by A2, Def8;
then (x \ y) \ (x \ (0. X)) = 0. X by Th4;
hence (x \ y) \ x = 0. X by Th2; :: thesis: verum