theorem Th20: :: GRNILP_1:20

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