for G being Group holds the_normal_subgroups_of G c= Subgroups G