theorem :: GROUP_5:72

for G being Group holds G ` = gr (commutators G) ;