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