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

proof

assume X is quasi-associative ; :: thesis: for x, y being Element of X holds (x \ y) ` = (y \ x) `
then for x being Element of X holds x ` <= x by Th71;
hence for x, y being Element of X holds (x \ y) ` = (y \ x) ` by Lm15; :: thesis: verum

end;

assume for x, y being Element of X holds (x \ y) ` = (y \ x) ` ; :: thesis: X is quasi-associative
then for x, y being Element of X holds (x `) \ y = (x \ y) ` by Lm16;
then for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X by Lm17;
hence X is quasi-associative by Lm18; :: thesis: verum