theorem :: GROUP_1A:178

for G being addGroup
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;