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 )

x = 0. X ; :: thesis: X is p-Semisimple

for x being Element of X holds (x `) ` = x

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 A2:
for x being Element of X st x ` = 0. X holds
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;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

x = 0. X ; :: thesis: X is p-Semisimple

for x being Element of X holds (x `) ` = x

proof

hence
X is p-Semisimple
by Th54; :: thesis: verum
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;(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