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

proof

assume A1: X is p-Semisimple ; :: thesis: for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u
let x, u, z be Element of X; :: thesis: z \ (z \ (x \ u)) = x \ u
(z \ (z \ (x \ u))) \ (x \ u) = 0. X by Th1
.= (x \ u) \ (x \ u) by Def5 ;
hence z \ (z \ (x \ u)) = x \ u by A1, Lm15; :: thesis: verum

end;

assume A2: for x, u, z being Element of X holds z \ (z \ (x \ u)) = x \ u ; :: thesis: X is p-Semisimple

now

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

end;

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