let a be Real; :: thesis: sin (((4 * PI) / 3) - a) = - (sin ((PI / 3) - a))
sin (((4 * PI) / 3) - a) = sin (PI + ((PI / 3) - a))
.= - (sin ((PI / 3) - a)) by SIN_COS:79 ;
hence sin (((4 * PI) / 3) - a) = - (sin ((PI / 3) - a)) ; :: thesis: verum