theorem Th114: :: GROUP_1A:160

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