theorem :: GROUP_1A:213
for G being addGroup
for a being Element of G
for A being Subset of G
for H being Subgroup of G holds (H + a) + A = H + (a + A)