theorem :: BCIIDEAL:27

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