PI / (- 4) > PI / (- 2) by XREAL_1:99;
then - (PI / 4) in { s where s is Real : ( - (PI / 2) < s & s < PI / 2 ) } ;
hence - (PI / 4) in ].(- (PI / 2)),(PI / 2).[ by RCOMP_1:def 2; :: thesis: verum