theorem :: GROUP_1A:148

for G being addGroup
for A being Subset of G
for H being Subgroup of G st G is Abelian addGroup holds
A + H = H + A by Th25;