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

proof

assume for I being Ideal of X holds I is commutative Ideal of X ; :: thesis: for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y)))
then X is commutative BCK-algebra by Th37;
hence for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) by BCIALG_3:4; :: thesis: verum

end;

assume for x, y being Element of X holds x \ (x \ y) = y \ (y \ (x \ (x \ y))) ; :: thesis: for I being Ideal of X holds I is commutative Ideal of X
then X is commutative BCK-algebra by BCIALG_3:4;
hence for I being Ideal of X holds I is commutative Ideal of X by Th37; :: thesis: verum