theorem Th48: :: BCIALG_1:48

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