theorem Th16: :: BCIALG_3:16

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