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; :: 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