let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x )
( ( for x being Element of X holds (x `) ` = x ) implies X is p-Semisimple )

proof

assume A1: for x being Element of X holds (x `) ` = x ; :: thesis: X is p-Semisimple

now :: thesis: for x, y being Element of X holds x \ (x \ y) = y

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

end;

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

end;

hence ( X is p-Semisimple iff for x being Element of X holds (x `) ` = x ) ; :: thesis: verum