theorem :: BCIALG_1:52

for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X holds x is atom )