theorem :: SIN_COS6:47

sin .: [.(PI / 2),((3 / 2) * PI).] = [.(- 1),1.] by COMPTRIG:31, RELAT_1:115;