theorem Th5: :: RLAFFIN1:5

for V being non empty add-associative addLoopStr
for A being Subset of V
for v, w being Element of V holds (v + w) + A = v + (w + A)