theorem :: BCIALG_1:69

for X being non empty BCIStr_0 holds
( X is p-Semisimple BCI-algebra iff for x, y, z being Element of X holds
( (x \ y) \ (x \ z) = z \ y & x \ (0. X) = x ) )