let X be BCK-algebra; :: thesis: ( X is p-Semisimple BCI-algebra implies {(0. X)} is commutative Ideal of X )
set X1 = {(0. X)};
A1: {(0. X)} c= the carrier of X

proof

let xx be object ; :: according to TARSKI:def 3 :: thesis: ( not xx in {(0. X)} or xx in the carrier of X )
assume xx in {(0. X)} ; :: thesis: xx in the carrier of X
then xx = 0. X by TARSKI:def 1;
hence xx in the carrier of X ; :: thesis: verum

end;

A2: for x, y being Element of X st x \ y in {(0. X)} & y in {(0. X)} holds
x in {(0. X)}

proof

set X1 = {(0. X)};
let x, y be Element of X; :: thesis: ( x \ y in {(0. X)} & y in {(0. X)} implies x in {(0. X)} )
assume ( x \ y in {(0. X)} & y in {(0. X)} ) ; :: thesis: x in {(0. X)}
then ( x \ y = 0. X & y = 0. X ) by TARSKI:def 1;
then x = 0. X by BCIALG_1:2;
hence x in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

0. X in {(0. X)} by TARSKI:def 1;
then reconsider X1 = {(0. X)} as Ideal of X by A1, A2, BCIALG_1:def 18;
assume A3: X is p-Semisimple BCI-algebra ; :: thesis: {(0. X)} is commutative Ideal of X
for x, y, z being Element of X st (x \ y) \ z in X1 & z in X1 holds
x \ (y \ (y \ x)) in X1

proof

let x, y, z be Element of X; :: thesis: ( (x \ y) \ z in X1 & z in X1 implies x \ (y \ (y \ x)) in X1 )
assume ( (x \ y) \ z in X1 & z in X1 ) ; :: thesis: x \ (y \ (y \ x)) in X1
then ( (x \ y) \ z = 0. X & z = 0. X ) by TARSKI:def 1;
then A4: x \ y = 0. X by BCIALG_1:2;
y is atom by A3, BCIALG_1:52;
then x = y by A4;
then x \ (y \ (y \ x)) = x \ (x \ (0. X)) by BCIALG_1:def 5;
then x \ (y \ (y \ x)) = x \ x by BCIALG_1:2;
then x \ (y \ (y \ x)) = 0. X by BCIALG_1:def 5;
hence x \ (y \ (y \ x)) in X1 by TARSKI:def 1; :: thesis: verum

end;

hence {(0. X)} is commutative Ideal of X by Def6; :: thesis: verum