:: deftheorem defines commutative BINOP_1:def 2 :
for A being set
for o being BinOp of A holds
( o is commutative iff for a, b being Element of A holds o . (a,b) = o . (b,a) );