:: deftheorem Def1 defines commutative BCIALG_3:def 1 :
for IT being non empty BCIStr_0 holds
( IT is commutative iff for x, y being Element of IT holds x \ (x \ y) = y \ (y \ x) );