theorem :: BCIALG_5:39

for X being BCI-algebra
for B, P being non empty Subset of X
for X being BCI-algebra st B = BCK-part X & P = p-Semisimple-part X holds
B /\ P = {(0. X)}