let X be BCI-algebra; :: thesis: ( X is alternative iff X is associative )
thus ( X is alternative implies X is associative ) :: thesis: ( X is associative implies X is alternative )

proof

assume A1: X is alternative ; :: thesis: X is associative
for x, y, z being Element of X holds (x \ y) \ z = x \ (y \ z)

proof

let x, y, z be Element of X; :: thesis: (x \ y) \ z = x \ (y \ z)
(((x \ y) \ y) \ ((x \ y) \ z)) \ (z \ y) = 0. X by Th1;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ y) \ (y \ z)) = 0. X by Th4;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ ((z \ (y \ z)) \ y) = 0. X by Th7;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z `) \ (y \ z)) \ y) = 0. X by A1, Th76;
then ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (((z `) \ (y \ z)) \ (y `)) = 0. X by A1, Th76;
then A2: ((((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z)) \ (0. X) = 0. X by Def3;
((x \ y) \ z) \ (x \ (y \ z)) = ((x \ y) \ (x \ (y \ z))) \ z by Th7;
then ((x \ y) \ z) \ (x \ (y \ z)) = ((x \ (x \ (y \ z))) \ y) \ z by Th7;
then ((x \ y) \ z) \ (x \ (y \ z)) = (((x \ x) \ (y \ z)) \ y) \ z by A1, Def27;
then ((x \ y) \ z) \ (x \ (y \ z)) = (((y \ z) `) \ y) \ z by Def5;
then ((x \ y) \ z) \ (x \ (y \ z)) = ((y \ z) \ y) \ z by A1, Th76;
then ((x \ y) \ z) \ (x \ (y \ z)) = ((y \ y) \ z) \ z by Th7;
then ((x \ y) \ z) \ (x \ (y \ z)) = (z `) \ z by Def5;
then A3: ((x \ y) \ z) \ (x \ (y \ z)) = 0. X by A1, Th76;
(x \ (y \ z)) \ ((x \ y) \ z) = (((x \ y) \ y) \ (y \ z)) \ ((x \ y) \ z) by A1, Th76
.= (((x \ y) \ y) \ ((x \ y) \ z)) \ (y \ z) by Th7 ;
then (x \ (y \ z)) \ ((x \ y) \ z) = 0. X by A2, Th2;
hence (x \ y) \ z = x \ (y \ z) by A3, Def7; :: thesis: verum

end;

hence X is associative by Def20; :: thesis: verum

end;

assume X is associative ; :: thesis: X is alternative
then for x, y being Element of X holds
( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) by Def20;
hence X is alternative by Def27; :: thesis: verum