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

proof

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

end;

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