let X be BCI-algebra; :: thesis: ( ( for X being BCI-algebra

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

assume for X being BCI-algebra

for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ; :: thesis: the carrier of X = BCK-part X

then X is BCK-algebra by BCIALG_1:15;

hence the carrier of X = BCK-part X by Th25; :: thesis: verum

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

assume for X being BCI-algebra

for x, y, z being Element of X holds (x \ y) \ y = (x \ z) \ (y \ z) ; :: thesis: the carrier of X = BCK-part X

then X is BCK-algebra by BCIALG_1:15;

hence the carrier of X = BCK-part X by Th25; :: thesis: verum