theorem :: BCIIDEAL:22

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