theorem Th3: :: BCIALG_3:3

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