theorem :: BCIALG_6:58

for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for K1 being Ideal of HK (G,RK)
for RK1 being I-congruence of HK (G,RK),K1
for I being Ideal of G
for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic