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

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

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

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

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

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

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

proof

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

(z \ x) ` = (x \ x) \ (z \ x) by Def5;

then (z \ x) ` = x \ z by A1;

hence (z `) \ (x `) = x \ z by Th9; :: thesis: verum

end;(z \ x) ` = (x \ x) \ (z \ x) by Def5;

then (z \ x) ` = x \ z by A1;

hence (z `) \ (x `) = x \ z by Th9; :: thesis: verum