theorem :: BCIALG_1:68

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