theorem Th17: :: SIN_COS5:17

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