:: deftheorem defines implicative BCIALG_4:def 15 :
for IT being BCK-Algebra_with_Condition(S) holds
( IT is implicative iff for x, y being Element of IT holds x \ (y \ x) = x );