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 )

then for x, y being Element of X holds x \ y = y \ x by Lm7;

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

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
for x being Element of X holds x ` = x
; :: thesis: X is associative
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;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

then for x, y being Element of X holds x \ y = y \ x by Lm7;

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