theorem Th8: :: RLAFFIN1:8

for S being non empty addLoopStr
for v being Element of S holds v + ({} S) = {} S