theorem Thm6: :: EUCLID10:12

for a being Real holds cos (((2 * PI) / 3) - a) = - (cos ((PI / 3) + a))