theorem Th8: :: BCIALG_3:8

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