theorem :: BCIIDEAL:42

for X being BCK-algebra holds
( {(0. X)} 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, Th36;