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