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

thus ( X is p-Semisimple implies for x, y being Element of X holds x \ (y `) = y \ (x `) ) by Th57; :: thesis: ( ( for x, y being Element of X holds x \ (y `) = y \ (x `) ) implies X is p-Semisimple )

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

thus ( X is p-Semisimple implies for x, y being Element of X holds x \ (y `) = y \ (x `) ) by Th57; :: thesis: ( ( for x, y being Element of X holds x \ (y `) = y \ (x `) ) implies X is p-Semisimple )

assume A1: for x, y being Element of X holds x \ (y `) = y \ (x `) ; :: 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 `) ` by A1;

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

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

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

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

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