:: deftheorem defines commutators GROUP_5:def 5 :
for G being Group
for H1, H2 being Subgroup of G holds commutators (H1,H2) = commutators ((carr H1),(carr H2));