theorem :: BCIALG_3:11

for X being BCK-algebra st X is commutative BCK-algebra holds
for x, y, a being Element of X st x <= a holds
(a \ y) \ ((a \ y) \ (a \ x)) = (a \ y) \ (x \ y) by Th8;