theorem Th62: :: BCIALG_1:62

for X being BCI-algebra holds
( X is p-Semisimple iff for x being Element of X st x ` = 0. X holds
x = 0. X )