let G be 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.]
let H1, H2, H3, H4 be Subgroup of G; ( H1 is Subgroup of H2 & H3 is Subgroup of H4 implies [.H1,H3.] is Subgroup of [.H2,H4.] )
assume
( H1 is Subgroup of H2 & H3 is Subgroup of H4 )
; [.H1,H3.] is Subgroup of [.H2,H4.]
then
commutators (H1,H3) c= commutators (H2,H4)
by Th56;
hence
[.H1,H3.] is Subgroup of [.H2,H4.]
by GROUP_4:32; verum