theorem :: BCIALG_3:42

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