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

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

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

for x, y being Element of X holds x \ (y `) = y \ (x `)

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

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

for x, y being Element of X holds x \ (y `) = y \ (x `)

proof

hence
X is p-Semisimple
by Th63; :: thesis: verum
let x, y be Element of X; :: thesis: x \ (y `) = y \ (x `)

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

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

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

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