theorem Th97: :: GROUP_1A:143
for G being addGroup
for A, B being Subset of G
for H being Subgroup of G holds (A + H) + B = A + (H + B) by Th10;