theorem Th51: :: BCIIDEAL:51

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