theorem Th29: :: BCIALG_3:29

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