theorem :: BCIALG_1:65

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