PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: PI > 0 by XXREAL_1:4;
A3: PI / (- 4) > PI / (- 2) by A1, XREAL_1:101;
- (PI / 4) in { s where s is Real : ( - (PI / 2) < s & s < PI / 2 ) } by A3;
hence - (PI / 4) in ].(- (PI / 2)),(PI / 2).[ by RCOMP_1:def 2; :: thesis: verum