thus Dihedral_group 1, INT.Group 2 are_isomorphic by Th73; :: thesis: Dihedral_group 1 is commutative
hence Dihedral_group 1 is commutative by GROUP_6:77; :: thesis: verum