let X be BCK-algebra; :: thesis: the carrier of X is commutative Ideal of X
set B = BCK-part X;
B0: the carrier of X = BCK-part X by P25010;
A2: BCK-part X is Ideal of X

proof

A1: 0. X in BCK-part X by BCIALG_1:19;
for x, y being Element of X st x \ y in BCK-part X & y in BCK-part X holds
x in BCK-part X

proof

let x, y be Element of X; :: thesis: ( x \ y in BCK-part X & y in BCK-part X implies x in BCK-part X )
assume A2: ( x \ y in BCK-part X & y in BCK-part X ) ; :: thesis: x in BCK-part X
consider x1 being Element of X such that
B1: ( x \ y = x1 & 0. X <= x1 ) by A2;
consider x2 being Element of X such that
B2: ( y = x2 & 0. X <= x2 ) by A2;
A7: (x \ y) ` = 0. X by B1, BCIALG_1:def 11;
(x ` ) \ (y ` ) = 0. X by A7, BCIALG_1:9;
then (x ` ) \ (0. X) = 0. X by B2, BCIALG_1:def 11;
then (0. X) \ x = 0. X by BCIALG_1:2;
then 0. X <= x by BCIALG_1:def 11;
hence x in BCK-part X ; :: thesis: verum

end;

hence BCK-part X is Ideal of X by A1, BCIALG_1:def 18; :: thesis: verum

end;

for x, y, z being Element of X st (x \ y) \ z in BCK-part X & z in BCK-part X holds
x \ (y \ (y \ x)) in BCK-part X

proof

let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in BCK-part X & z in BCK-part X implies x \ (y \ (y \ x)) in BCK-part X )
assume ( (x \ y) \ z in BCK-part X & z in BCK-part X ) ; :: thesis: x \ (y \ (y \ x)) in BCK-part X
(0. X) \ (x \ (y \ (y \ x))) = (x \ (y \ (y \ x))) `
.= 0. X by BCIALG_1:def 8 ;
then 0. X <= x \ (y \ (y \ x)) by BCIALG_1:def 11;
hence x \ (y \ (y \ x)) in BCK-part X ; :: thesis: verum

end;

hence the carrier of X is commutative Ideal of X by A2, Def4, B0; :: thesis: verum