theorem Th135: :: GROUP_1A:334

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