theorem :: GROUP_6:26

for G being Group
for N being normal Subgroup of G holds card (G ./. N) = Index N ;