theorem Th133: :: GROUP_1A:179

for G being addGroup
for a being Element of G
for H being finite Subgroup of G ex B, C being finite set st
( B = a + H & C = H + a & card H = card B & card H = card C )