let G be Group; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: [.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; :: thesis: verum

[.H1,H3.] is Subgroup of [.H2,H4.]

let H1, H2, H3, H4 be Subgroup of G; :: thesis: ( 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 ) ; :: thesis: [.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; :: thesis: verum