theorem Th6: :: BCIALG_3:6

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