theorem :: BCIALG_1:60

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