theorem Th120: :: GROUP_1A:166

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