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