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