theorem :: BCIALG_6:52

for X being BCI-algebra
for K being closed Ideal of X
for RK being I-congruence of X,K holds Ker (nat_hom RK) = K