theorem :: SIN_COS9:5

tan | ].(- (PI / 2)),(PI / 2).[ is continuous by Lm1, FDIFF_1:25;