for X, X9 being BCI-algebra
for A9 being non empty Subset of X9
for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds
f " A9 is closed Ideal of X