let G be Group; :: thesis: for H1, H2 being Subgroup of G holds 1_ G in commutators H1,H2
let H1, H2 be Subgroup of G; :: thesis: 1_ G in commutators H1,H2
A1: 1_ G in H2 by GROUP_2:55;
( [.(1_ G),(1_ G).] = 1_ G & 1_ G in H1 ) by Th22, GROUP_2:55;
hence 1_ G in commutators H1,H2 by A1, Th58; :: thesis: verum