theorem Th37: :: BCIALG_2:37

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