theorem Th50: :: BCIIDEAL:50

for X being BCK-algebra
for I being Ideal of X holds
( I is implicative-ideal of X iff for x, y being Element of X st x \ (y \ x) in I holds
x in I )