theorem Th57: :: BCIALG_1:57

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