theorem :: BCIIDEAL:48

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