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