let X be BCI-algebra; :: thesis: ( X is associative implies X is weakly-positive-implicative )
assume A1: X is associative ; :: thesis: X is weakly-positive-implicative
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 \ y) \ z = x \ (y \ z) by A1;
then (x \ y) \ z = (x \ (0. X)) \ (y \ z) by Th2;
then (x \ y) \ z = (x \ (z \ z)) \ (y \ z) by Def5;
hence (x \ y) \ z = ((x \ z) \ z) \ (y \ z) by A1; :: thesis: verum

end;

hence X is weakly-positive-implicative ; :: thesis: verum