theorem ThA33: :: GROUP_1A:79

for G being non empty addMagma
for A being Subset of G
for g, h being Element of G st G is add-associative holds
(g + A) + h = g + (A + h) by Th10;