cos ((2 * PI) / 3) = cos (((2 * PI) / 3) - 0)
.= - (cos ((PI / 3) + 0)) by Thm6
.= - (cos (PI / 3)) ;
hence cos ((2 * PI) / 3) = - (1 / 2) by Thm8; :: thesis: verum