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
commutators (H1,H3) c= commutators (H2,H4)
let H1, H2, H3, H4 be Subgroup of G; :: thesis: ( H1 is Subgroup of H2 & H3 is Subgroup of H4 implies commutators (H1,H3) c= commutators (H2,H4) )
assume ( H1 is Subgroup of H2 & H3 is Subgroup of H4 ) ; :: thesis: commutators (H1,H3) c= commutators (H2,H4)
then ( the carrier of H1 c= the carrier of H2 & the carrier of H3 c= the carrier of H4 ) by GROUP_2:def 5;
hence commutators (H1,H3) c= commutators (H2,H4) by Th50; :: thesis: verum