theorem Th16: :: SIN_COS4:16

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