sin ((2 * PI) / 3) = sin (((2 * PI) / 3) - 0)
.= sin ((PI / 3) + 0) by Thm5
.= sin (PI / 3) ;
hence sin ((2 * PI) / 3) = (sqrt 3) / 2 by Thm9; :: thesis: verum