theorem :: BCIALG_5:41

for X being BCI-algebra
for B being non empty Subset of X
for X being BCI-algebra st B = BCK-part X holds
( X is p-Semisimple BCI-algebra iff B = {(0. X)} )