theorem :: GROUP_1A:163

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