theorem :: BCIIDEAL:12

for X being associative BCI-algebra
for A being Ideal of X holds A is closed