theorem :: SIN_COS5:23

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