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

proof

assume A1: X is p-Semisimple ; :: thesis: for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x)
let x, y, z be Element of X; :: thesis: x \ (z \ y) = y \ (z \ x)
y \ (z \ x) = (z \ (z \ y)) \ (z \ x) by A1;
then A2: (y \ (z \ x)) \ (x \ (z \ y)) = 0. X by Th1;
x \ (z \ y) = (z \ (z \ x)) \ (z \ y) by A1;
then (x \ (z \ y)) \ (y \ (z \ x)) = 0. X by Th1;
hence x \ (z \ y) = y \ (z \ x) by A2, Def7; :: thesis: verum

end;

assume A3: for x, y, z being Element of X holds x \ (z \ y) = y \ (z \ x) ; :: thesis: X is p-Semisimple
for x being Element of X holds (x `) ` = x

proof

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

end;

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