for G being Group
for G1 being Subgroup of G
for N being strict normal Subgroup of G st N is Subgroup of G1 & G1 ./. ((G1,N) `*`) is Subgroup of center (G ./. N) holds
[.G1,((Omega). G).] is Subgroup of N