for A, C being non empty set
for L being commutative BinOp of A
for LC being BinOp of C st C c= A & LC = L || C holds
LC is commutative