theorem :: BCIALG_3:10

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