theorem :: BCIIDEAL:49

for X being BCK-algebra st ( for I being Ideal of X holds I is commutative Ideal of X ) holds
( ( for x, y being Element of X holds
( x \ y = x iff y \ (y \ x) = 0. X ) ) & ( for x, y being Element of X st x \ y = x holds
y \ x = y ) & ( for x, y, a being Element of X st y <= a holds
(a \ x) \ (a \ y) = y \ x ) & ( for x, y being Element of X holds
( x \ (y \ (y \ x)) = x \ y & (x \ y) \ ((x \ y) \ x) = x \ y ) ) & ( for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) ) )