:: deftheorem Def5 defines BCI-weakly-commutative BCIALG_3:def 5 :
for IT being BCI-algebra holds
( IT is BCI-weakly-commutative iff for x, y being Element of IT holds (x \ (x \ y)) \ ((0. IT) \ (x \ y)) = y \ (y \ x) );