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 Th55; :: thesis: verum