theorem :: EUCLID10:9

for a being Real holds sin (((3 * PI) / 2) + a) = - (sin ((PI / 2) - a))