theorem :: SIN_COS5:21

for x being Real holds (cos x) ^2 = (1 + (cos (2 * x))) / 2