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