theorem :: BCIIDEAL:45

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) ) by BCIALG_3:1, Th37;