theorem :: GROUP_1A:169

for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( carr H c= (H + a) + (H + (- a)) & carr H c= (H + (- a)) + (H + a) )