theorem :: BCIALG_1:18

for X being BCI-algebra holds
( X is being_K iff X is BCK-algebra )