theorem Thm7: :: EUCLID10:13

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