theorem Th130: :: GROUP_3:130

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