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 )

( ( for x being Element of X holds (x `) ` = x ) implies X is p-Semisimple )

proof

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

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

hence
X is p-Semisimple
; :: thesis: verumlet 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;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