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 Th62;
hence [.H1,H3.] is Subgroup of [.H2,H4.] by GROUP_4:41; :: thesis: verum