x is strict Subgroup of G by GROUP_3:def 1;
hence x is strict normal Subgroup of G by GROUP_3:116; :: thesis: verum