let X be BCK-algebra; :: thesis: ( X is commutative BCK-algebra iff for I being Ideal of X holds I is commutative Ideal of X )
thus ( X is commutative BCK-algebra implies for I being Ideal of X holds I is commutative Ideal of X ) :: thesis: ( ( for I being Ideal of X holds I is commutative Ideal of X ) implies X is commutative BCK-algebra )

proof

assume A: X is commutative BCK-algebra ; :: thesis: for I being Ideal of X holds I is commutative Ideal of X
{(0. X)} is commutative Ideal of X by TL254, A;
hence for I being Ideal of X holds I is commutative Ideal of X by TL253; :: thesis: verum

end;

assume A: for I being Ideal of X holds I is commutative Ideal of X ; :: thesis: X is commutative BCK-algebra
{(0. X)} is commutative Ideal of X by TL253, A;
hence X is commutative BCK-algebra by TL254; :: thesis: verum