for G being Group
for a being Element of G
for H being Subgroup of G holds
( card H = card (a * H) & card H = card (H * a) ) by Th131, CARD_1:5;