for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X being Subset of T
for x, y being Point of T holds (X + x) + y = X + (x + y)