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