for G being Group
for H being Subgroup of G
for N being normal Subgroup of G st N is Subgroup of H holds
ex M being strict Subgroup of G st the carrier of M = N ` H