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

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