theorem Th18: :: SIN_COS4:18

for th1, th2 being Real holds (cos th1) - (cos th2) = - (2 * ((sin ((th1 + th2) / 2)) * (sin ((th1 - th2) / 2))))