theorem Th71: :: BCIALG_1:71

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