for X being non empty right_complementable add-associative right_zeroed addLoopStr
for M being Subset of X
for x being Point of X st x in M holds
0. X in (- x) + M