theorem Th4: :: BCIALG_4:5

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