theorem Th17: :: GROUP_5:17

for G being Group
for a, b being Element of G holds [.a,b.] = ((b * a) ") * (a * b)