theorem :: BCIALG_1:61

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