theorem Th73: :: GROUP_1A:274

for G being addGroup st G is Abelian addGroup holds
for H being strict Subgroup of G
for a being Element of G holds H * a = H