the strict normal Subgroup of G in the_normal_subgroups_of G by Def1;
hence not the_normal_subgroups_of G is empty ; :: thesis: verum