theorem Th51: :: BCIALG_2:51

for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds X ./. RI is BCI-algebra