PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then PI / 4 < PI / 2 by XREAL_1:78;
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