theorem :: BCIALG_4:52

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