for G being Group
for H1, H2 being Subgroup of G holds 1_ G in commutators (H1,H2)