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:46;
( [.(1_ G),(1_ G).] = 1_ G & 1_ G in H1 ) by Th19, GROUP_2:46;
hence 1_ G in commutators (H1,H2) by A1, Th52; :: thesis: verum