theorem :: BCIALG_4:42

for X being non empty BCIStr_1 holds
( X is commutative BCK-Algebra_with_Condition(S) iff for x, y, z being Element of X holds
( x \ ((0. X) \ y) = x & (x \ z) \ (x \ y) = (y \ z) \ (y \ x) & (x \ y) \ z = x \ (y * z) ) )