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