theorem :: BCIALG_6:48

for X, X9 being BCI-algebra
for CI being closed Ideal of X
for f being BCI-homomorphism of X,X9 st f is onto holds
f .: CI is closed Ideal of X9