theorem Th61: :: GROUP_5:61

for x being set
for G being Group
for A, B being Subset of G holds
( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )