theorem :: GROUP_5:63

for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] = gr (commutators (H1,H2)) ;