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

proof

assume A1: X is p-Semisimple ; :: thesis: for x being Element of X st x ` = 0. X holds
x = 0. X
let x be Element of X; :: thesis: ( x ` = 0. X implies x = 0. X )
assume x ` = 0. X ; :: thesis: x = 0. X
then (x ` ) ` = 0. X by Def5;
hence x = 0. X by A1, Def26; :: thesis: verum

end;

assume A2: for x being Element of X st x ` = 0. X holds
x = 0. 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 ` ) ` )) ` = (x ` ) \ (((x ` ) ` ) ` ) by Th9
.= (x ` ) \ (x ` ) by Th8
.= 0. X by Def5 ;
then A3: x \ ((x ` ) ` ) = 0. X by A2;
((x ` ) ` ) \ x = 0. X by Th1;
hence (x ` ) ` = x by A3, Def7; :: thesis: verum

end;

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