theorem Th145: :: GROUP_1A:191

for G being addGroup
for H being Subgroup of G holds
( Index H = card (Left_Cosets H) & Index H = card (Right_Cosets H) ) by Th136, CARD_1:5;