theorem :: GROUP_24:92

for n being non zero Nat holds card (Dihedral_group n) = 2 * n