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

let x, y be Element of X; :: thesis: x \ (x \ y) = y
A2: 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 ;
(x \ (x \ y)) \ y = 0. X by Th1;
hence x \ (x \ y) = y by A2, Def7; :: thesis: verum

end;

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

end;

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