for G being addGroup
for H being strict Subgroup of G holds card (con_class H) = Index (Normalizer H)