theorem :: BCIALG_1:70

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