theorem :: BCIIDEAL:46

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 \ y = x \ (y \ (y \ x)) ) by BCIALG_3:3, Th37;