theorem :: SIN_COS5:25

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