for G being Group
for a being Element of G
for H being Subgroup of G holds
( H is finite iff H |^ a is finite )