theorem Th45: :: SIN_COS6:45
sin .: [.(- (PI / 2)),(PI / 2).] = [.(- 1),1.] by COMPTRIG:30, RELAT_1:115;