theorem :: BCIIDEAL:20

for X being BCI-algebra holds BCK-part X is p-ideal of X