let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y )
( X is p-Semisimple iff for x, y being Element of X holds y \ (y \ x) = x ) ;
hence ( X is p-Semisimple iff for x, y, z being Element of X holds (z \ y) \ (z \ x) = x \ y ) by Lm8; :: thesis: verum