theorem Th53: :: BCIIDEAL:53

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