let X be BCI-algebra; :: thesis: ( ( for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ) implies the carrier of X = BCK-part X )
assume for X being BCI-algebra
for x, y being Element of X holds (x \ y) \ ((x \ y) \ (y \ x)) = 0. X ; :: thesis: the carrier of X = BCK-part X
then X is BCK-algebra by BCIALG_1:17;
hence the carrier of X = BCK-part X by Th25; :: thesis: verum