theorem :: GRNILP_1:13

for G being Group
for H, H1, H2 being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds
[.(H1 /\ H),H.] is Subgroup of H2 /\ H