theorem Th72: :: BCIALG_1:72

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