:: deftheorem defines [. GROUP_5:def 7 :
for G being Group
for A, B being Subset of G holds [.A,B.] = gr (commutators (A,B));