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 )

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

thus ( X is being_K implies X is BCK-algebra ) :: thesis: ( X is BCK-algebra implies X is being_K )

proof

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

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

hence
X is BCK-algebra
by Def8; :: thesis: verumlet 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;(s `) \ (0. X) = 0. X by A1;

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

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