theorem :: BCIALG_1:53

for X being BCI-algebra st X is p-Semisimple holds
BCK-part X = {(0. X)}