theorem Thm18: :: EUCLID10:29

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