theorem :: BCIIDEAL:18

for X being BCI-algebra
for X1 being non empty Subset of X st X1 is p-ideal of X holds
X1 is Ideal of X