for X, X9 being BCI-algebra
for H9 being SubAlgebra of X9
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X9 st I = Ker f & the carrier of H9 = rng f holds
X ./. RI,H9 are_isomorphic