theorem :: BCIALG_1:58

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