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