let X be BCK-algebra; :: thesis: ( {(0. X)} is commutative Ideal of X iff X is commutative BCK-algebra )
thus ( {(0. X)} is commutative Ideal of X implies X is commutative BCK-algebra ) :: thesis: ( X is commutative BCK-algebra implies {(0. X)} is commutative Ideal of X )

proof

assume A: {(0. X)} is commutative Ideal of X ; :: thesis: X is commutative BCK-algebra
for x, y being Element of X st x <= y holds
x = y \ (y \ x)

proof

let x, y be Element of X; :: thesis: ( x <= y implies x = y \ (y \ x) )
assume x <= y ; :: thesis: x = y \ (y \ x)
then B2: x \ y = 0. X by BCIALG_1:def 11;
B4: (y \ (y \ x)) \ x = 0. X by BCIALG_1:1;
x \ y in {(0. X)} by B2, TARSKI:def 1;
then x \ (y \ (y \ x)) in {(0. X)} by A, TL251;
then x \ (y \ (y \ x)) = 0. X by TARSKI:def 1;
hence x = y \ (y \ x) by B4, BCIALG_1:def 7; :: thesis: verum

end;

hence X is commutative BCK-algebra by BCIALG_3:5; :: thesis: verum

end;

assume A: X is commutative BCK-algebra ; :: thesis: {(0. X)} is commutative Ideal of X
A1: ( X is commutative BCK-algebra implies for x, y being Element of X holds x \ y = x \ (y \ (y \ x)) )

proof

assume A2: X is commutative BCK-algebra ; :: thesis: for x, y being Element of X holds x \ y = x \ (y \ (y \ x))
let x, y be Element of X; :: thesis: x \ y = x \ (y \ (y \ x))
x \ y = x \ (x \ (x \ y)) by BCIALG_1:8
.= x \ (y \ (y \ x)) by A2, BCIALG_3:def 1 ;
hence x \ y = x \ (y \ (y \ x)) ; :: thesis: verum

end;

for x, y being Element of X st x \ y in {(0. X)} holds
x \ (y \ (y \ x)) in {(0. X)} by A, A1;
hence {(0. X)} is commutative Ideal of X by TL251, BCIALG_1:43; :: thesis: verum