theorem Th112: :: GROUP_1A:158

for G being addGroup
for a being Element of G
for H being Subgroup of G st G is Abelian addGroup holds
a + H = H + a by Th25;