theorem Thm4: :: EUCLID10:8

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