theorem :: GROUP_1A:208

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