theorem :: BCIALG_3:9

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