let x0, x1 be Real; :: thesis: [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1))
[!cos,x0,x1!] = ((cos x0) - (cos x1)) / (x0 - x1)
.= (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1) by SIN_COS4:18 ;
hence [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)) by XCMPLX_1:187; :: thesis: verum