theorem :: GROUP_1A:146

for G being addGroup
for A being Subset of G
for H1, H2 being Subgroup of G holds (H1 + A) + H2 = H1 + (A + H2) by Th10;