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

proof

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

proof

let x, y, z be Element of X; :: thesis: x \ (z \ y) = y \ (z \ x)
(x \ (0. X)) \ (z \ y) = (y \ (0. X)) \ (z \ x) by A1;
then x \ (z \ y) = (y \ (0. X)) \ (z \ x) by Th2;
hence x \ (z \ y) = y \ (z \ x) by Th2; :: thesis: verum

end;

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

end;