theorem Th7: :: RLTOPSP1:7

for X being non empty add-associative addLoopStr
for x being Point of X
for M, N being Subset of X holds (x + M) + N = x + (M + N)