:: deftheorem defines Dihedral_group GROUP_24:def 9 :
for n being non natural ExtNat holds Dihedral_group n = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group));