theorem :: BCIALG_1:43

for X being BCI-algebra holds {(0. X)} is closed Ideal of X