theorem :: SIN_COS5:24

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