theorem Th122: :: GROUP_24:116

for n being non zero even Nat
for k being Nat st n = 2 * k & n > 2 holds
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for g being Element of (Dihedral_group n) holds
( g in center (Dihedral_group n) iff ( g = 1_ (Dihedral_group n) or g = x |^ k ) )