theorem Th21: :: BCIIDEAL:21

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