theorem :: SIN_COS5:22

for x being Real holds (sin x) |^ 3 = ((3 * (sin x)) - (sin (3 * x))) / 4