theorem Th121: :: GROUP_1A:167

for G being addGroup
for a, b being Element of G
for H being Subgroup of G holds
( H + a = H + b iff H + a meets H + b )