theorem :: BCIIDEAL:39

for X being BCK-algebra
for I being Ideal of X
for x, y being Element of X st x \ (x \ y) in I holds
( x \ ((x \ y) \ ((x \ y) \ x)) in I & (y \ (y \ x)) \ x in I & (y \ (y \ x)) \ (x \ y) in I )