theorem :: BCIALG_2:52

for X being BCI-algebra
for I being Ideal of X st I = BCK-part X holds
for RI being I-congruence of X,I holds X ./. RI is p-Semisimple BCI-algebra