theorem :: BCIALG_2:41

for X being BCI-algebra
for A, I being Ideal of X
for IA being I-congruence of X,A
for II being I-congruence of X,I st Class (IA,(0. X)) = Class (II,(0. X)) holds
IA = II