for X being BCI-algebra
for i, j, k being Nat st X is BCI-algebra of i,j,j + k,i + k holds
X is BCK-algebra