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