theorem Th130: :: GROUP_1A:329

for G being addGroup
for A being Subset of G holds card (con_class A) = Index (Normalizer A)