theorem Th47: :: BCIALG_1:47

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