theorem Th132: :: GROUP_1A:331

for G being addGroup
for a being Element of G holds card (con_class a) = Index (Normalizer {a})