theorem :: BCIALG_1:20

for X being BCI-algebra
for x, y being Element of BCK-part X holds x \ y in BCK-part X