for X, X9 being BCI-algebra
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 & f is onto holds
X ./. RI,X9 are_isomorphic