:: deftheorem Def24 defines implicative BCIALG_1:def 24 :
for IT being BCI-algebra holds
( IT is implicative iff for x, y being Element of IT holds (x \ (x \ y)) \ (y \ x) = y \ (y \ x) );