theorem Th131: :: GROUP_1A:177

for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( carr H,a + H are_equipotent & carr H,H + a are_equipotent )