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