theorem :: GROUP_5:66

for G being Group
for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
[.H1,H3.] is Subgroup of [.H2,H4.]