theorem :: BCIIDEAL:47

for X being BCK-algebra holds
( ( 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))) ) by BCIALG_3:4, Th37;