theorem :: GROUP_1A:145

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