:: deftheorem defines commutators GROUP_5:def 6 :
for G being Group holds commutators G = commutators (((Omega). G),((Omega). G));