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)

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

hence
X is weakly-positive-implicative
; :: thesis: verum
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;(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