for A being set
for D being non empty set
for o being BinOp of D st o is uniquely-decomposable holds
(o,D) .: A is uniquely-decomposable