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 & the carrier of H1 = carr H1 & the carrier of H2 = carr H2 & the carrier of H3 = carr H3 & the carrier of H4 = carr H4 & commutators H1,H3 = commutators (carr H1),(carr H3) & commutators H2,H4 = commutators (carr H2),(carr H4) ) by GROUP_2:def 5;
hence commutators H1,H3 c= commutators H2,H4 by Th55; :: thesis: verum