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 )

then for x, y being Element of X holds

( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) ;

hence X is alternative ; :: thesis: verum

thus ( X is alternative implies X is associative ) :: thesis: ( X is associative implies X is alternative )

proof

assume
X is associative
; :: thesis: X is alternative
assume A1:
X is alternative
; :: thesis: X is associative

for x, y, z being Element of X holds (x \ y) \ z = x \ (y \ z)

end;for x, y, z being Element of X holds (x \ y) \ z = x \ (y \ z)

proof

hence
X is associative
; :: thesis: verum
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;

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;(((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;

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

then for x, y being Element of X holds

( x \ (x \ y) = (x \ x) \ y & (x \ y) \ y = x \ (y \ y) ) ;

hence X is alternative ; :: thesis: verum