let X be BCI-algebra; :: thesis: ( X is p-Semisimple BCI-algebra implies X is weakly-positive-implicative BCI-algebra )
assume A1: X is p-Semisimple BCI-algebra ; :: thesis: X is weakly-positive-implicative BCI-algebra
for x, y, z being Element of X holds (x \ y) \ z = ((x \ z) \ z) \ (y \ z)

proof

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

end;

hence X is weakly-positive-implicative BCI-algebra by Def23; :: thesis: verum