theorem :: GROUP_1A:322

for G being addGroup
for H being strict Subgroup of G holds
( H is normal Subgroup of G iff con_class H = {H} )