for G being Group
for H, F2 being Subgroup of G
for F1 being normal Subgroup of F2
for G2 being Subgroup of G st G2 = F2 /\ H holds
for G1 being normal Subgroup of G2 st G1 = F1 /\ H holds
ex G3 being Subgroup of F2 ./. F1 st G2 ./. G1,G3 are_isomorphic