theorem :: SIN_COS:79

for th being Real holds
( sin (th + (2 * PI)) = sin th & cos (th + (2 * PI)) = cos th & sin ((PI / 2) - th) = cos th & cos ((PI / 2) - th) = sin th & sin ((PI / 2) + th) = cos th & cos ((PI / 2) + th) = - (sin th) & sin (PI + th) = - (sin th) & cos (PI + th) = - (cos th) ) by Th77;