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

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