theorem :: SIN_COS5:20

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