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