theorem Th122: :: GROUP_1A:168
for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds (H + a) + b c= (H + a) + (H + b)