theorem Th40: :: BCIALG_3:40

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