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