let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x ` ) )
thus ( X is p-Semisimple implies for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x ` ) ) by Lm14; :: thesis: ( ( for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x ` ) ) implies X is p-Semisimple )
assume A1: for x, y, z being Element of X holds x \ (y \ z) = (z \ y) \ (x ` ) ; :: thesis: X is p-Semisimple
for x, y being Element of X holds x \ (y ` ) = y \ (x ` )

proof

let x, y be Element of X; :: thesis: x \ (y ` ) = y \ (x ` )
x \ (y ` ) = (y \ (0. X)) \ (x ` ) by A1;
hence x \ (y ` ) = y \ (x ` ) by Th2; :: thesis: verum

end;

hence X is p-Semisimple by Th63; :: thesis: verum