theorem Thm5: :: EUCLID10:11

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