theorem :: GROUP_1A:209

for G being addGroup
for a being Element of G
for H being Subgroup of G holds H + a = H + {a} ;