theorem Th28: :: BCIALG_3:28

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