theorem :: DIFF_2:57

for x0, x1 being Real holds [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1)