theorem Th73: :: BCIALG_1:73
for X being BCI-algebra holds
( X is quasi-associative iff for x, y being Element of X holds (x `) \ y = (x \ y) ` )