theorem Th65: :: GROUP_1A:266

for G being addGroup
for a being Element of G
for H being Subgroup of G holds
( H is finite iff H * a is finite )