let X be BCI-algebra; ( 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; ( ( 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)
; X is p-Semisimple
for x, z being Element of X holds (z `) \ (x `) = x \ z
hence
X is p-Semisimple
by Th59; verum