n = +infty by COUNTERS:2;
hence for b₁ being strict Group holds
( b₁ = Dihedral_group n iff b₁ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) by DefDihedral; :: thesis: verum