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