(5 * PI) / 3 = PI + ((2 * PI) / 3) ;
hence cos ((5 * PI) / 3) = - (cos ((2 * PI) / 3)) by SIN_COS:79
.= 1 / 2 by EUCLID10:23 ;
:: thesis: verum