theorem :: BCIALG_1:45

for X being BCI-algebra holds BCK-part X is closed Ideal of X