theorem :: SIN_COS6:52

cos .: ].PI,(2 * PI).[ = ].(- 1),1.[