theorem :: BCIALG_5:43

for X being BCI-algebra
for j, m, n being Nat st X is p-Semisimple BCI-algebra holds
X is BCI-algebra of n + j,n,m,(m + j) + 1