PI / 4 < PI / 2 by XREAL_1:76;
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