theorem Thm3: :: EUCLID10:7

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