let X be BCK-algebra; :: thesis: ( {(0. X)} is commutative Ideal of X iff for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) )
thus ( {(0. X)} is commutative Ideal of X implies for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) :: thesis: ( ( for x, y being Element of X holds x \ (x \ y) <= y \ (y \ x) ) implies {(0. X)} is commutative Ideal of X )

proof

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

end;

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