theorem Th59: :: BCIALG_1:59

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