theorem :: BCIALG_6:49

for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds nat_hom RI is onto