theorem :: BCIALG_1:13

for X being BCI-algebra st ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ y = x \ y ) holds
X is BCK-algebra