theorem Th102: :: GROUP_24:97
for n being non zero Nat
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 k being Nat st k <> 0 & k < n holds
x |^ k <> 1_ (Dihedral_group n)