let X be BCI-algebra; :: thesis: ( ( for x, y being Element of X holds y \ x = x \ y ) iff X is associative )

thus ( ( for x, y being Element of X holds y \ x = x \ y ) implies X is associative ) by Lm6; :: thesis: ( X is associative implies for x, y being Element of X holds y \ x = x \ y )

assume X is associative ; :: thesis: for x, y being Element of X holds y \ x = x \ y

then for x being Element of X holds x ` = x by Th47;

hence for x, y being Element of X holds y \ x = x \ y by Lm7; :: thesis: verum

thus ( ( for x, y being Element of X holds y \ x = x \ y ) implies X is associative ) by Lm6; :: thesis: ( X is associative implies for x, y being Element of X holds y \ x = x \ y )

assume X is associative ; :: thesis: for x, y being Element of X holds y \ x = x \ y

then for x being Element of X holds x ` = x by Th47;

hence for x, y being Element of X holds y \ x = x \ y by Lm7; :: thesis: verum