theorem :: SIN_COS6:51

cos .: [.PI,(2 * PI).] = [.(- 1),1.] by COMPTRIG:33, RELAT_1:115;