theorem :: BCIALG_1:74
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x \ y) \ (y \ x) in BCK-part X )