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