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