let X be BCI-algebra; :: thesis: ( X is p-Semisimple iff for x, z being Element of X holds (z `) \ (x `) = x \ z )
thus ( X is p-Semisimple implies for x, z being Element of X holds (z `) \ (x `) = x \ z ) by Lm10; :: thesis: ( ( for x, z being Element of X holds (z `) \ (x `) = x \ z ) implies X is p-Semisimple )
assume A1: for x, z being Element of X holds (z `) \ (x `) = x \ z ; :: thesis: X is p-Semisimple
for x being Element of X holds (x `) ` = x

proof

let x be Element of X; :: thesis: (x `) ` = x
((0. X) `) \ (x `) = x \ (0. X) by A1;
then (x `) ` = x \ (0. X) by Th2;
hence (x `) ` = x by Th2; :: thesis: verum

end;

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