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 )

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

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 )

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

now :: thesis: for x being Element of X holds (x `) ` = x

hence
X is p-Semisimple
by Th54; :: thesis: verumlet x be Element of X; :: thesis: (x `) ` = x

((x \ (0. X)) `) ` = x \ (0. X) by A1;

then ((x \ (0. X)) `) ` = x by Th2;

hence (x `) ` = x by Th2; :: thesis: verum

end;((x \ (0. X)) `) ` = x \ (0. X) by A1;

then ((x \ (0. X)) `) ` = x by Th2;

hence (x `) ` = x by Th2; :: thesis: verum