for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )