:: deftheorem Def11 defines BCK-positive-implicative BCIALG_3:def 11 :
for IT being BCK-algebra holds
( IT is BCK-positive-implicative iff for x, y, z being Element of IT holds (x \ y) \ z = (x \ z) \ (y \ z) );