let X be BCI-algebra; :: thesis: ( X is associative iff for x being Element of X holds x ` = x )
thus ( X is associative implies for x being Element of X holds x ` = x ) :: thesis: ( ( for x being Element of X holds x ` = x ) implies X is associative )

proof

assume A1: X is associative ; :: thesis: for x being Element of X holds x ` = x
let x be Element of X; :: thesis: x ` = x
A2: x \ (x `) = (x \ (0. X)) \ x by A1
.= x \ x by Th2
.= 0. X by Def5 ;
(x `) \ x = (x \ x) ` by A1
.= (0. X) ` by Def5
.= 0. X by Def5 ;
hence x ` = x by A2, Def7; :: thesis: verum

end;

assume for x being Element of X holds x ` = x ; :: thesis: X is associative
then for x, y being Element of X holds x \ y = y \ x by Lm7;
hence X is associative by Lm6; :: thesis: verum