let a be Real; :: thesis: cos (((2 * PI) / 3) - a) = - (cos ((PI / 3) + a))
cos (((2 * PI) / 3) - a) = cos (PI - ((PI / 3) + a))
.= ((cos PI) * (cos ((PI / 3) + a))) + ((sin PI) * (sin ((PI / 3) + a))) by SIN_COS:83
.= - (cos ((PI / 3) + a)) by SIN_COS:77 ;
hence cos (((2 * PI) / 3) - a) = - (cos ((PI / 3) + a)) ; :: thesis: verum