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