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