theorem :: BCIIDEAL:31

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