theorem :: GROUP_5:39

for G being Group
for a, b being Element of G holds
( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )