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