theorem :: BCIIDEAL:29

for X being BCI-algebra st ( for X being BCI-algebra
for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ) holds
the carrier of X = BCK-part X