theorem :: GROUP_1A:147

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