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

proof

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) \ (x \ x) by A1;
then (z \ x) ` = (x \ z) \ (0. X) by Def5;
then (z \ x) ` = x \ z by Th2;
hence (z `) \ (x `) = x \ z by Th9; :: thesis: verum

end;

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